:: XBOOLE_0 semantic presentation

scheme :: XBOOLE_0:sch 1
s1{ F1() -> set , P1[ set ] } :
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 in F1() & P1[b2] ) )
proof end;

definition
func {} -> set means :Def1: :: XBOOLE_0:def 1
for b1 being set holds not b1 in a1;
existence
ex b1 being set st
for b2 being set holds not b2 in b1
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds not b3 in b1 ) & ( for b3 being set holds not b3 in b2 ) holds
b1 = b2
proof end;
let c1, c2 be set ;
func c1 \/ c2 -> set means :Def2: :: XBOOLE_0:def 2
for b1 being set holds
( b1 in a3 iff ( b1 in a1 or b1 in a2 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 in c1 or b2 in c2 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ( b3 in c1 or b3 in c2 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 in c1 or b3 in c2 ) ) ) holds
b1 = b2
proof end;
commutativity
for b1, b2, b3 being set st ( for b4 being set holds
( b4 in b1 iff ( b4 in b2 or b4 in b3 ) ) ) holds
for b4 being set holds
( b4 in b1 iff ( b4 in b3 or b4 in b2 ) ) ;
idempotence
for b1, b2 being set holds
( b2 in b1 iff ( b2 in b1 or b2 in b1 ) ) ;
func c1 /\ c2 -> set means :Def3: :: XBOOLE_0:def 3
for b1 being set holds
( b1 in a3 iff ( b1 in a1 & b1 in a2 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 in c1 & b2 in c2 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ( b3 in c1 & b3 in c2 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 in c1 & b3 in c2 ) ) ) holds
b1 = b2
proof end;
commutativity
for b1, b2, b3 being set st ( for b4 being set holds
( b4 in b1 iff ( b4 in b2 & b4 in b3 ) ) ) holds
for b4 being set holds
( b4 in b1 iff ( b4 in b3 & b4 in b2 ) ) ;
idempotence
for b1, b2 being set holds
( b2 in b1 iff ( b2 in b1 & b2 in b1 ) ) ;
func c1 \ c2 -> set means :Def4: :: XBOOLE_0:def 4
for b1 being set holds
( b1 in a3 iff ( b1 in a1 & not b1 in a2 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 in c1 & not b2 in c2 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ( b3 in c1 & not b3 in c2 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 in c1 & not b3 in c2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines {} XBOOLE_0:def 1 :
for b1 being set holds
( b1 = {} iff for b2 being set holds not b2 in b1 );

:: deftheorem Def2 defines \/ XBOOLE_0:def 2 :
for b1, b2, b3 being set holds
( b3 = b1 \/ b2 iff for b4 being set holds
( b4 in b3 iff ( b4 in b1 or b4 in b2 ) ) );

:: deftheorem Def3 defines /\ XBOOLE_0:def 3 :
for b1, b2, b3 being set holds
( b3 = b1 /\ b2 iff for b4 being set holds
( b4 in b3 iff ( b4 in b1 & b4 in b2 ) ) );

:: deftheorem Def4 defines \ XBOOLE_0:def 4 :
for b1, b2, b3 being set holds
( b3 = b1 \ b2 iff for b4 being set holds
( b4 in b3 iff ( b4 in b1 & not b4 in b2 ) ) );

definition
let c1 be set ;
attr a1 is empty means :Def5: :: XBOOLE_0:def 5
a1 = {} ;
let c2 be set ;
func c1 \+\ c2 -> set equals :: XBOOLE_0:def 6
(a1 \ a2) \/ (a2 \ a1);
correctness
coherence
(c1 \ c2) \/ (c2 \ c1) is set ;
;
commutativity
for b1, b2, b3 being set st b1 = (b2 \ b3) \/ (b3 \ b2) holds
b1 = (b3 \ b2) \/ (b2 \ b3) ;
pred c1 misses c2 means :Def7: :: XBOOLE_0:def 7
a1 /\ a2 = {} ;
symmetry
for b1, b2 being set st b1 /\ b2 = {} holds
b2 /\ b1 = {} ;
pred c1 c< c2 means :: XBOOLE_0:def 8
( a1 c= a2 & a1 <> a2 );
irreflexivity
for b1 being set holds
( not b1 c= b1 or not b1 <> b1 ) ;
asymmetry
for b1, b2 being set st b1 c= b2 & b1 <> b2 & b2 c= b1 holds
not b2 <> b1
proof end;
pred c1,c2 are_c=-comparable means :: XBOOLE_0:def 9
( a1 c= a2 or a2 c= a1 );
reflexivity
for b1 being set holds
( b1 c= b1 or b1 c= b1 ) ;
symmetry
for b1, b2 being set holds
( ( not b1 c= b2 & not b2 c= b1 ) or b2 c= b1 or b1 c= b2 ) ;
redefine pred c1 = c2 means :: XBOOLE_0:def 10
( a1 c= a2 & a2 c= a1 );
compatibility
( c1 = c2 iff ( c1 c= c2 & c2 c= c1 ) )
proof end;
end;

:: deftheorem Def5 defines empty XBOOLE_0:def 5 :
for b1 being set holds
( b1 is empty iff b1 = {} );

:: deftheorem Def6 defines \+\ XBOOLE_0:def 6 :
for b1, b2 being set holds b1 \+\ b2 = (b1 \ b2) \/ (b2 \ b1);

:: deftheorem Def7 defines misses XBOOLE_0:def 7 :
for b1, b2 being set holds
( b1 misses b2 iff b1 /\ b2 = {} );

:: deftheorem Def8 defines c< XBOOLE_0:def 8 :
for b1, b2 being set holds
( b1 c< b2 iff ( b1 c= b2 & b1 <> b2 ) );

:: deftheorem Def9 defines are_c=-comparable XBOOLE_0:def 9 :
for b1, b2 being set holds
( b1,b2 are_c=-comparable iff ( b1 c= b2 or b2 c= b1 ) );

:: deftheorem Def10 defines = XBOOLE_0:def 10 :
for b1, b2 being set holds
( b1 = b2 iff ( b1 c= b2 & b2 c= b1 ) );

notation
let c1, c2 be set ;
antonym c1 meets c2 for c1 misses c2;
end;

theorem Th1: :: XBOOLE_0:1
for b1, b2, b3 being set holds
( b1 in b2 \+\ b3 iff ( ( b1 in b2 & not b1 in b3 ) or ( b1 in b3 & not b1 in b2 ) ) )
proof end;

theorem Th2: :: XBOOLE_0:2
for b1, b2, b3 being set st ( for b4 being set holds
( not b4 in b1 iff ( b4 in b2 iff b4 in b3 ) ) ) holds
b1 = b2 \+\ b3
proof end;

registration
cluster {} -> empty ;
coherence
{} is empty by Def5;
cluster empty set ;
existence
ex b1 being set st b1 is empty
proof end;
cluster non empty set ;
existence
not for b1 being set holds b1 is empty
proof end;
end;

registration
let c1 be non empty set ;
let c2 be set ;
cluster a1 \/ a2 -> non empty ;
coherence
not c1 \/ c2 is empty
proof end;
cluster a2 \/ a1 -> non empty ;
coherence
not c2 \/ c1 is empty ;
end;

theorem Th3: :: XBOOLE_0:3
for b1, b2 being set holds
( b1 meets b2 iff ex b3 being set st
( b3 in b1 & b3 in b2 ) )
proof end;

theorem Th4: :: XBOOLE_0:4
for b1, b2 being set holds
( b1 meets b2 iff ex b3 being set st b3 in b1 /\ b2 )
proof end;

theorem Th5: :: XBOOLE_0:5
for b1, b2, b3 being set st b1 misses b2 & b3 in b1 \/ b2 & not ( b3 in b1 & not b3 in b2 ) holds
( b3 in b2 & not b3 in b1 ) by Def2, Th3;

scheme :: XBOOLE_0:sch 2
s2{ F1() -> set , F2() -> set , P1[ set ] } :
F1() = F2()
provided
E8: for b1 being set holds
( b1 in F1() iff P1[b1] ) and
E9: for b1 being set holds
( b1 in F2() iff P1[b1] )
proof end;

scheme :: XBOOLE_0:sch 3
s3{ P1[ set ] } :
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff P1[b3] ) ) & ( for b3 being set holds
( b3 in b2 iff P1[b3] ) ) holds
b1 = b2
proof end;