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

proof

let a be object ; :: 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 )
reconsider aa = a as set by TARSKI:1;
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
A2: a = x /\ S and
x meets S ;
aa c= S by A2, XBOOLE_1:17;
hence a in bool S ; :: thesis: verum

end;

A3: 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 object ; :: 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
A4: x in Y and
A5: Y in { (x /\ S) where x is Element of P : x meets S } by TARSKI:def 4;
thus x in S by A4, A1, A5; :: thesis: verum

end;

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

proof

let s be object ; :: 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 A6: 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 4;
then consider p being set such that
A7: s in p and
A8: p in P by TARSKI:def 4;
p meets S by A7, A6, XBOOLE_0:3;
then A9: p /\ S in { (x /\ S) where x is Element of P : x meets S } by A8;
s in p /\ S by A7, A6, XBOOLE_0:def 4;
hence s in union { (x /\ S) where x is Element of P : x meets S } by A9, TARSKI:def 4; :: thesis: verum

end;

end;

now :: thesis: for A being Subset of S st A in { (x /\ S) where x is Element of P : x meets S } holds
( A <> {} & ( for B being Subset of S holds
( not B in { (x /\ S) where x is Element of P : x meets S } or A = B or A misses B ) ) )

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
A10: A = x /\ S and
A11: x meets S ;
consider z being object such that
A12: z in x and
A13: z in S by A11, XBOOLE_0:3;
reconsider Xp1 = X as non empty set by A13;
reconsider Pp1 = P as a_partition of Xp1 ;
thus A <> {} by A12, A13, A10, 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
A14: B = y /\ S and
y meets S ;
A15: ( x in Pp1 & y in Pp1 ) ;

per cases ( x = y or x misses y ) by A15, EQREL_1:def 4;

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

hence ( A = B or A misses B ) by A10, A14; :: thesis: verum

end;

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

hence ( A = B or A misses B ) by A10, A14, 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 A1, A3, EQREL_1:def 4; :: thesis: verum