set D = { (x /\ S) where x is Element of P : x meets S } ;
A: { (x /\ S) where x is Element of P : x meets S } c= bool S

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (x /\ S) where x is Element of P : x meets S } or a in bool S )
assume a in { (x /\ S) where x is Element of P : x meets S } ; :: thesis: a in bool S
then consider x being Element of P such that
A1: a = x /\ S and
x meets S ;
a c= S by A1, XBOOLE_1:17;
hence a in bool S ; :: thesis: verum

end;

B: union { (x /\ S) where x is Element of P : x meets S } = S

proof

thus union { (x /\ S) where x is Element of P : x meets S } c= S :: according to XBOOLE_0:def 10 :: thesis: S c= union { (x /\ S) where x is Element of P : x meets S }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (x /\ S) where x is Element of P : x meets S } or x in S )
assume x in union { (x /\ S) where x is Element of P : x meets S } ; :: thesis: x in S
then consider Y being set such that
A1: x in Y and
B1: Y in { (x /\ S) where x is Element of P : x meets S } by TARSKI:def 4;
thus x in S by A1, A, B1; :: thesis: verum

end;

thus S c= union { (x /\ S) where x is Element of P : x meets S } :: thesis: verum

proof

let s be set ; :: according to TARSKI:def 3 :: thesis: ( not s in S or s in union { (x /\ S) where x is Element of P : x meets S } )
assume A0: s in S ; :: thesis: s in union { (x /\ S) where x is Element of P : x meets S }
then s in X ;
then s in union P by EQREL_1:def 6;
then consider p being set such that
A1: s in p and
B1: p in P by TARSKI:def 4;
p meets S by A1, A0, XBOOLE_0:3;
then C1: p /\ S in { (x /\ S) where x is Element of P : x meets S } by B1;
s in p /\ S by A1, A0, XBOOLE_0:def 4;
hence s in union { (x /\ S) where x is Element of P : x meets S } by C1, TARSKI:def 4; :: thesis: verum

end;

end;

now

let A be Subset of S; :: thesis: ( A in { (x /\ S) where x is Element of P : x meets S } implies ( A <> {} & ( for B being Subset of S holds
( not B in { (x /\ S) where x is Element of P : x meets S } or b₂ = b₃ or b₂ misses b₃ ) ) ) )
assume A in { (x /\ S) where x is Element of P : x meets S } ; :: thesis: ( A <> {} & ( for B being Subset of S holds
( not B in { (x /\ S) where x is Element of P : x meets S } or b₂ = b₃ or b₂ misses b₃ ) ) )
then consider x being Element of P such that
B1: A = x /\ S and
C1: x meets S ;
consider z being set such that
D1: z in x and
E1: z in S by C1, XBOOLE_0:3;
reconsider Xp1 = X as non empty set by E1;
reconsider Pp1 = P as a_partition of Xp1 ;
thus A <> {} by D1, E1, B1, XBOOLE_0:def 4; :: thesis: for B being Subset of S holds
( not B in { (x /\ S) where x is Element of P : x meets S } or b₂ = b₃ or b₂ misses b₃ )
let B be Subset of S; :: thesis: ( not B in { (x /\ S) where x is Element of P : x meets S } or b₁ = b₂ or b₁ misses b₂ )
assume B in { (x /\ S) where x is Element of P : x meets S } ; :: thesis: ( b₁ = b₂ or b₁ misses b₂ )
then consider y being Element of P such that
G1: B = y /\ S and
y meets S ;
I1: ( x in Pp1 & y in Pp1 ) ;

per cases ( x = y or x misses y ) by I1, EQREL_1:def 6;

suppose x = y ; :: thesis: ( b₁ = b₂ or b₁ misses b₂ )

hence ( A = B or A misses B ) by B1, G1; :: thesis: verum

end;

suppose x misses y ; :: thesis: ( b₁ = b₂ or b₁ misses b₂ )

hence ( A = B or A misses B ) by B1, G1, XBOOLE_1:76; :: thesis: verum

end;

end;

end;

hence { (x /\ S) where x is Element of P : x meets S } is a_partition of S by A, B, EQREL_1:def 6; :: thesis: verum