let X be set ; :: thesis: for S being cup-closed cap-closed with_empty_element Subset-Family of X holds
( semidiff S is cap-closed & semidiff S is diff-finite-partition-closed )
let S be cup-closed cap-closed with_empty_element Subset-Family of X; :: thesis: ( semidiff S is cap-closed & semidiff S is diff-finite-partition-closed )
thus semidiff S is cap-closed :: thesis: semidiff S is diff-finite-partition-closed

proof

let s1, s2 be set ; :: according to FINSUB_1:def 2 :: thesis: ( not s1 in semidiff S or not s2 in semidiff S or s1 /\ s2 in semidiff S )
assume A1: ( s1 in semidiff S & s2 in semidiff S ) ; :: thesis: s1 /\ s2 in semidiff S
then consider a1, b1 being Element of S such that
A2: s1 = a1 \ b1 by LemX1;
consider a2, b2 being Element of S such that
A3: s2 = a2 \ b2 by A1, LemX1;
A4: s1 /\ s2 = ((a1 \ b1) /\ a2) \ b2 by A2, A3, XBOOLE_1:49
.= ((a1 /\ a2) \ b1) \ b2 by XBOOLE_1:49
.= (a1 /\ a2) \ (b1 \/ b2) by XBOOLE_1:41 ;
( a1 /\ a2 is Element of S & b1 \/ b2 is Element of S ) by FINSUB_1:def 1, FINSUB_1:def 2;
hence s1 /\ s2 in semidiff S by A4, SETFAM_1:def 6; :: thesis: verum

end;

thus semidiff S is diff-finite-partition-closed :: thesis: verum

proof

let s1, s2 be Element of semidiff S; :: according to SRINGS_1:def 2 :: thesis: ( s1 \ s2 is empty or ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2 )
assume A5: not s1 \ s2 is empty ; :: thesis: ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2
consider a1, b1 being Element of S such that
A6: s1 = a1 \ b1 by LemX1;
consider a2, b2 being Element of S such that
A7: s2 = a2 \ b2 by LemX1;
A8: a1 /\ b2 in S by FINSUB_1:def 2;
a1 /\ a2 in S by FINSUB_1:def 2;
then A9: (a1 /\ a2) /\ b2 in S by FINSUB_1:def 2;
A10: b1 \/ a2 in S by FINSUB_1:def 1;
then A11: (b1 \/ a2) \/ b2 in S by FINSUB_1:def 1;
A12: s1 \ s2 = (((a1 /\ b2) \ (b1 \/ a2)) \/ (a1 \ ((b1 \/ a2) \/ b2))) \/ (((a1 /\ a2) /\ b2) \ b1) by A6, A7, Thm04;
A13: ( (a1 /\ b2) \ (b1 \/ a2) c= s1 \ s2 & a1 \ ((b1 \/ a2) \/ b2) c= s1 \ s2 & ((a1 /\ a2) /\ b2) \ b1 c= s1 \ s2 )

proof

A14: ((a1 /\ b2) \ (b1 \/ a2)) \/ (a1 \ ((b1 \/ a2) \/ b2)) c= s1 \ s2 by A12, XBOOLE_1:7;
( (a1 /\ b2) \ (b1 \/ a2) c= ((a1 /\ b2) \ (b1 \/ a2)) \/ (a1 \ ((b1 \/ a2) \/ b2)) & a1 \ ((b1 \/ a2) \/ b2) c= ((a1 /\ b2) \ (b1 \/ a2)) \/ (a1 \ ((b1 \/ a2) \/ b2)) ) by XBOOLE_1:7;
hence ( (a1 /\ b2) \ (b1 \/ a2) c= s1 \ s2 & a1 \ ((b1 \/ a2) \/ b2) c= s1 \ s2 & ((a1 /\ a2) /\ b2) \ b1 c= s1 \ s2 ) by A12, A14, XBOOLE_1:7; :: thesis: verum

end;

per cases ( ( (a1 /\ b2) \ (b1 \/ a2) <> {} & a1 \ ((b1 \/ a2) \/ b2) <> {} & ((a1 /\ a2) /\ b2) \ b1 <> {} ) or ( (a1 /\ b2) \ (b1 \/ a2) = {} & a1 \ ((b1 \/ a2) \/ b2) <> {} & ((a1 /\ a2) /\ b2) \ b1 <> {} ) or ( (a1 /\ b2) \ (b1 \/ a2) <> {} & a1 \ ((b1 \/ a2) \/ b2) <> {} & ((a1 /\ a2) /\ b2) \ b1 = {} ) or ( (a1 /\ b2) \ (b1 \/ a2) <> {} & a1 \ ((b1 \/ a2) \/ b2) = {} & ((a1 /\ a2) /\ b2) \ b1 <> {} ) or ( (a1 /\ b2) \ (b1 \/ a2) <> {} & a1 \ ((b1 \/ a2) \/ b2) = {} & ((a1 /\ a2) /\ b2) \ b1 = {} ) or ( (a1 /\ b2) \ (b1 \/ a2) = {} & a1 \ ((b1 \/ a2) \/ b2) <> {} & ((a1 /\ a2) /\ b2) \ b1 = {} ) or ( (a1 /\ b2) \ (b1 \/ a2) = {} & a1 \ ((b1 \/ a2) \/ b2) = {} & ((a1 /\ a2) /\ b2) \ b1 <> {} ) ) by A5, A12;

suppose A16: ( (a1 /\ b2) \ (b1 \/ a2) <> {} & a1 \ ((b1 \/ a2) \/ b2) <> {} & ((a1 /\ a2) /\ b2) \ b1 <> {} ) ; :: thesis: ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2

set x = {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)};
a17: {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} c= semidiff S

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} or t in semidiff S )
assume t in {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} ; :: thesis: t in semidiff S
then ( t = (a1 /\ b2) \ (b1 \/ a2) or t = a1 \ ((b1 \/ a2) \/ b2) or t = ((a1 /\ a2) /\ b2) \ b1 ) by ENUMSET1:def 1;
hence t in semidiff S by A8, A10, A11, A9, SETFAM_1:def 6; :: thesis: verum

end;

{((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} or t in bool (s1 \ s2) )
assume A18: t in {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} ; :: thesis: t in bool (s1 \ s2)
then reconsider t1 = t as set ;
t1 c= s1 \ s2 by A13, A18, ENUMSET1:def 1;
hence t in bool (s1 \ s2) ; :: thesis: verum

end;

then reconsider x = {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} as Subset-Family of (s1 \ s2) ;
x is a_partition of s1 \ s2

proof

thus union x = s1 \ s2 by A12, Thm05; :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or ( not b₁ = {} & ( for b₂ being Element of bool (s1 \ s2) holds
( not b₂ in x or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let u be Subset of (s1 \ s2); :: thesis: ( not u in x or ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) ) )
assume A19: u in x ; :: thesis: ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) )
then A20: ( u = (a1 /\ b2) \ (b1 \/ a2) or u = a1 \ ((b1 \/ a2) \/ b2) or u = ((a1 /\ a2) /\ b2) \ b1 ) by ENUMSET1:def 1;
thus u <> {} by A19, A16; :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ )
let v be Subset of (s1 \ s2); :: thesis: ( not v in x or u = v or u misses v )
assume v in x ; :: thesis: ( u = v or u misses v )
then ( v = (a1 /\ b2) \ (b1 \/ a2) or v = a1 \ ((b1 \/ a2) \/ b2) or v = ((a1 /\ a2) /\ b2) \ b1 ) by ENUMSET1:def 1;
hence ( u = v or u misses v ) by A20, Thm01; :: thesis: verum

end;

hence ex x being finite Subset of (semidiff S) st x is a_partition of s1 \ s2 by a17; :: thesis: verum

end;

suppose A20a: ( (a1 /\ b2) \ (b1 \/ a2) = {} & a1 \ ((b1 \/ a2) \/ b2) <> {} & ((a1 /\ a2) /\ b2) \ b1 <> {} ) ; :: thesis: ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2

set x = {(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)};
a21: {(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} c= semidiff S

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} or t in semidiff S )
assume t in {(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} ; :: thesis: t in semidiff S
then ( t = a1 \ ((b1 \/ a2) \/ b2) or t = ((a1 /\ a2) /\ b2) \ b1 ) by TARSKI:def 2;
hence t in semidiff S by A11, A9, SETFAM_1:def 6; :: thesis: verum

end;

{(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} or t in bool (s1 \ s2) )
assume A22: t in {(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} ; :: thesis: t in bool (s1 \ s2)
then reconsider t1 = t as set ;
( a1 \ ((b1 \/ a2) \/ b2) c= s1 \ s2 & ((a1 /\ a2) /\ b2) \ b1 c= s1 \ s2 )

proof

A23: ((a1 /\ b2) \ (b1 \/ a2)) \/ (a1 \ ((b1 \/ a2) \/ b2)) c= s1 \ s2 by A12, XBOOLE_1:7;
( (a1 /\ b2) \ (b1 \/ a2) c= ((a1 /\ b2) \ (b1 \/ a2)) \/ (a1 \ ((b1 \/ a2) \/ b2)) & a1 \ ((b1 \/ a2) \/ b2) c= ((a1 /\ b2) \ (b1 \/ a2)) \/ (a1 \ ((b1 \/ a2) \/ b2)) ) by XBOOLE_1:7;
hence ( a1 \ ((b1 \/ a2) \/ b2) c= s1 \ s2 & ((a1 /\ a2) /\ b2) \ b1 c= s1 \ s2 ) by A12, A23, XBOOLE_1:7; :: thesis: verum

end;

then t1 c= s1 \ s2 by A22, TARSKI:def 2;
hence t in bool (s1 \ s2) ; :: thesis: verum

end;

then reconsider x = {(a1 \ ((b1 \/ a2) \/ b2)),(((a1 /\ a2) /\ b2) \ b1)} as Subset-Family of (s1 \ s2) ;
x is a_partition of s1 \ s2

proof

thus union x = s1 \ s2 by A12, A20a, ZFMISC_1:75; :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or ( not b₁ = {} & ( for b₂ being Element of bool (s1 \ s2) holds
( not b₂ in x or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let u be Subset of (s1 \ s2); :: thesis: ( not u in x or ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) ) )
assume A25: u in x ; :: thesis: ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) )
then A26: ( u = a1 \ ((b1 \/ a2) \/ b2) or u = ((a1 /\ a2) /\ b2) \ b1 ) by TARSKI:def 2;
thus u <> {} by A25, A20a; :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ )
let v be Subset of (s1 \ s2); :: thesis: ( not v in x or u = v or u misses v )
assume v in x ; :: thesis: ( u = v or u misses v )
then ( v = a1 \ ((b1 \/ a2) \/ b2) or v = ((a1 /\ a2) /\ b2) \ b1 ) by TARSKI:def 2;
hence ( u = v or u misses v ) by A26, Thm01; :: thesis: verum

end;

hence ex x being finite Subset of (semidiff S) st x is a_partition of s1 \ s2 by a21; :: thesis: verum

end;

suppose A26a: ( (a1 /\ b2) \ (b1 \/ a2) <> {} & a1 \ ((b1 \/ a2) \/ b2) <> {} & ((a1 /\ a2) /\ b2) \ b1 = {} ) ; :: thesis: ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2

set x = {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2))};
a27: {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2))} c= semidiff S

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2))} or t in semidiff S )
assume t in {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2))} ; :: thesis: t in semidiff S
then ( t = (a1 /\ b2) \ (b1 \/ a2) or t = a1 \ ((b1 \/ a2) \/ b2) ) by TARSKI:def 2;
hence t in semidiff S by SETFAM_1:def 6, A8, A10, A11; :: thesis: verum

end;

{((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2))} c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2))} or t in bool (s1 \ s2) )
assume A28: t in {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2))} ; :: thesis: t in bool (s1 \ s2)
then reconsider t1 = t as set ;
t1 c= s1 \ s2 by A13, A28, TARSKI:def 2;
hence t in bool (s1 \ s2) ; :: thesis: verum

end;

then reconsider x = {((a1 /\ b2) \ (b1 \/ a2)),(a1 \ ((b1 \/ a2) \/ b2))} as Subset-Family of (s1 \ s2) ;
x is a_partition of s1 \ s2

proof

thus union x = s1 \ s2 by A12, A26a, ZFMISC_1:75; :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or ( not b₁ = {} & ( for b₂ being Element of bool (s1 \ s2) holds
( not b₂ in x or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let u be Subset of (s1 \ s2); :: thesis: ( not u in x or ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) ) )
assume A29: u in x ; :: thesis: ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) )
then A30: ( u = (a1 /\ b2) \ (b1 \/ a2) or u = a1 \ ((b1 \/ a2) \/ b2) ) by TARSKI:def 2;
thus u <> {} by A29, A26a; :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ )
let v be Subset of (s1 \ s2); :: thesis: ( not v in x or u = v or u misses v )
assume v in x ; :: thesis: ( u = v or u misses v )
then ( v = (a1 /\ b2) \ (b1 \/ a2) or v = a1 \ ((b1 \/ a2) \/ b2) ) by TARSKI:def 2;
hence ( u = v or u misses v ) by A30, Thm01; :: thesis: verum

end;

hence ex x being finite Subset of (semidiff S) st x is a_partition of s1 \ s2 by a27; :: thesis: verum

end;

suppose A31: ( (a1 /\ b2) \ (b1 \/ a2) <> {} & a1 \ ((b1 \/ a2) \/ b2) = {} & ((a1 /\ a2) /\ b2) \ b1 <> {} ) ; :: thesis: ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2

set x = {((a1 /\ b2) \ (b1 \/ a2)),(((a1 /\ a2) /\ b2) \ b1)};
a32: {((a1 /\ b2) \ (b1 \/ a2)),(((a1 /\ a2) /\ b2) \ b1)} c= semidiff S

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((a1 /\ b2) \ (b1 \/ a2)),(((a1 /\ a2) /\ b2) \ b1)} or t in semidiff S )
assume t in {((a1 /\ b2) \ (b1 \/ a2)),(((a1 /\ a2) /\ b2) \ b1)} ; :: thesis: t in semidiff S
then ( t = (a1 /\ b2) \ (b1 \/ a2) or t = ((a1 /\ a2) /\ b2) \ b1 ) by TARSKI:def 2;
hence t in semidiff S by A8, A9, A10, SETFAM_1:def 6; :: thesis: verum

end;

{((a1 /\ b2) \ (b1 \/ a2)),(((a1 /\ a2) /\ b2) \ b1)} c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((a1 /\ b2) \ (b1 \/ a2)),(((a1 /\ a2) /\ b2) \ b1)} or t in bool (s1 \ s2) )
assume A33: t in {((a1 /\ b2) \ (b1 \/ a2)),(((a1 /\ a2) /\ b2) \ b1)} ; :: thesis: t in bool (s1 \ s2)
then reconsider t1 = t as set ;
t1 c= s1 \ s2 by A13, A33, TARSKI:def 2;
hence t in bool (s1 \ s2) ; :: thesis: verum

end;

then reconsider x = {((a1 /\ b2) \ (b1 \/ a2)),(((a1 /\ a2) /\ b2) \ b1)} as Subset-Family of (s1 \ s2) ;
x is a_partition of s1 \ s2

proof

thus union x = s1 \ s2 by A12, A31, ZFMISC_1:75; :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or ( not b₁ = {} & ( for b₂ being Element of bool (s1 \ s2) holds
( not b₂ in x or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let u be Subset of (s1 \ s2); :: thesis: ( not u in x or ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) ) )
assume A34: u in x ; :: thesis: ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) )
then A35: ( u = (a1 /\ b2) \ (b1 \/ a2) or u = ((a1 /\ a2) /\ b2) \ b1 ) by TARSKI:def 2;
thus u <> {} by A31, A34; :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ )
let v be Subset of (s1 \ s2); :: thesis: ( not v in x or u = v or u misses v )
assume v in x ; :: thesis: ( u = v or u misses v )
then ( v = (a1 /\ b2) \ (b1 \/ a2) or v = ((a1 /\ a2) /\ b2) \ b1 ) by TARSKI:def 2;
hence ( u = v or u misses v ) by A35, Thm01; :: thesis: verum

end;

hence ex x being finite Subset of (semidiff S) st x is a_partition of s1 \ s2 by a32; :: thesis: verum

end;

suppose A36: ( (a1 /\ b2) \ (b1 \/ a2) <> {} & a1 \ ((b1 \/ a2) \/ b2) = {} & ((a1 /\ a2) /\ b2) \ b1 = {} ) ; :: thesis: ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2

set x = {((a1 /\ b2) \ (b1 \/ a2))};
a37: {((a1 /\ b2) \ (b1 \/ a2))} c= semidiff S

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((a1 /\ b2) \ (b1 \/ a2))} or t in semidiff S )
assume t in {((a1 /\ b2) \ (b1 \/ a2))} ; :: thesis: t in semidiff S
then t = (a1 /\ b2) \ (b1 \/ a2) by TARSKI:def 1;
hence t in semidiff S by SETFAM_1:def 6, A8, A10; :: thesis: verum

end;

{((a1 /\ b2) \ (b1 \/ a2))} c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((a1 /\ b2) \ (b1 \/ a2))} or t in bool (s1 \ s2) )
assume A38: t in {((a1 /\ b2) \ (b1 \/ a2))} ; :: thesis: t in bool (s1 \ s2)
then reconsider t1 = t as set ;
t1 c= s1 \ s2 by A13, A38, TARSKI:def 1;
hence t in bool (s1 \ s2) ; :: thesis: verum

end;

then reconsider x = {((a1 /\ b2) \ (b1 \/ a2))} as Subset-Family of (s1 \ s2) ;
x is a_partition of s1 \ s2

proof

thus union x = s1 \ s2 by A12, A36; :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or ( not b₁ = {} & ( for b₂ being Element of bool (s1 \ s2) holds
( not b₂ in x or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let u be Subset of (s1 \ s2); :: thesis: ( not u in x or ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) ) )
assume A39: u in x ; :: thesis: ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) )
then A40: u = (a1 /\ b2) \ (b1 \/ a2) by TARSKI:def 1;
thus u <> {} by A39, A36; :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ )
thus for v being Subset of (s1 \ s2) holds
( not v in x or u = v or u misses v ) by A40, TARSKI:def 1; :: thesis: verum

end;

hence ex x being finite Subset of (semidiff S) st x is a_partition of s1 \ s2 by a37; :: thesis: verum

end;

suppose A41: ( (a1 /\ b2) \ (b1 \/ a2) = {} & a1 \ ((b1 \/ a2) \/ b2) <> {} & ((a1 /\ a2) /\ b2) \ b1 = {} ) ; :: thesis: ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2

set x = {(a1 \ ((b1 \/ a2) \/ b2))};
a42: {(a1 \ ((b1 \/ a2) \/ b2))} c= semidiff S

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {(a1 \ ((b1 \/ a2) \/ b2))} or t in semidiff S )
assume t in {(a1 \ ((b1 \/ a2) \/ b2))} ; :: thesis: t in semidiff S
then t = a1 \ ((b1 \/ a2) \/ b2) by TARSKI:def 1;
hence t in semidiff S by SETFAM_1:def 6, A11; :: thesis: verum

end;

{(a1 \ ((b1 \/ a2) \/ b2))} c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {(a1 \ ((b1 \/ a2) \/ b2))} or t in bool (s1 \ s2) )
assume A43: t in {(a1 \ ((b1 \/ a2) \/ b2))} ; :: thesis: t in bool (s1 \ s2)
then reconsider t1 = t as set ;
t1 c= s1 \ s2 by A13, A43, TARSKI:def 1;
hence t in bool (s1 \ s2) ; :: thesis: verum

end;

then reconsider x = {(a1 \ ((b1 \/ a2) \/ b2))} as Subset-Family of (s1 \ s2) ;
x is a_partition of s1 \ s2

proof

thus union x = s1 \ s2 by A12, A41; :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or ( not b₁ = {} & ( for b₂ being Element of bool (s1 \ s2) holds
( not b₂ in x or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let u be Subset of (s1 \ s2); :: thesis: ( not u in x or ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) ) )
assume A44: u in x ; :: thesis: ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) )
then A45: u = a1 \ ((b1 \/ a2) \/ b2) by TARSKI:def 1;
thus u <> {} by A44, A41; :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ )
thus for v being Subset of (s1 \ s2) holds
( not v in x or u = v or u misses v ) by A45, TARSKI:def 1; :: thesis: verum

end;

hence ex x being finite Subset of (semidiff S) st x is a_partition of s1 \ s2 by a42; :: thesis: verum

end;

suppose A46: ( (a1 /\ b2) \ (b1 \/ a2) = {} & a1 \ ((b1 \/ a2) \/ b2) = {} & ((a1 /\ a2) /\ b2) \ b1 <> {} ) ; :: thesis: ex b₁ being Element of bool (semidiff S) st b₁ is a_partition of s1 \ s2

set x = {(((a1 /\ a2) /\ b2) \ b1)};
a47: {(((a1 /\ a2) /\ b2) \ b1)} c= semidiff S

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {(((a1 /\ a2) /\ b2) \ b1)} or t in semidiff S )
assume t in {(((a1 /\ a2) /\ b2) \ b1)} ; :: thesis: t in semidiff S
then t = ((a1 /\ a2) /\ b2) \ b1 by TARSKI:def 1;
hence t in semidiff S by SETFAM_1:def 6, A9; :: thesis: verum

end;

{(((a1 /\ a2) /\ b2) \ b1)} c= bool (s1 \ s2)

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {(((a1 /\ a2) /\ b2) \ b1)} or t in bool (s1 \ s2) )
assume A48: t in {(((a1 /\ a2) /\ b2) \ b1)} ; :: thesis: t in bool (s1 \ s2)
then reconsider t1 = t as set ;
t1 c= s1 \ s2 by A13, A48, TARSKI:def 1;
hence t in bool (s1 \ s2) ; :: thesis: verum

end;

then reconsider x = {(((a1 /\ a2) /\ b2) \ b1)} as Subset-Family of (s1 \ s2) ;
x is a_partition of s1 \ s2

proof

thus union x = s1 \ s2 by A12, A46; :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or ( not b₁ = {} & ( for b₂ being Element of bool (s1 \ s2) holds
( not b₂ in x or b₁ = b₂ or b₁ misses b₂ ) ) ) )
let u be Subset of (s1 \ s2); :: thesis: ( not u in x or ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) ) )
assume A49: u in x ; :: thesis: ( not u = {} & ( for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ ) ) )
then A50: u = ((a1 /\ a2) /\ b2) \ b1 by TARSKI:def 1;
thus u <> {} by A49, A46; :: thesis: for b₁ being Element of bool (s1 \ s2) holds
( not b₁ in x or u = b₁ or u misses b₁ )
thus for v being Subset of (s1 \ s2) holds
( not v in x or u = v or u misses v ) by A50, TARSKI:def 1; :: thesis: verum

end;

hence ex x being finite Subset of (semidiff S) st x is a_partition of s1 \ s2 by a47; :: thesis: verum

end;

end;

end;