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 b2 = b3 or b2 misses b3 ) ) ) )
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 b2 = b3 or b2 misses b3 ) ) )
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 b2 = b3 or b2 misses b3 )
let B be Subset of S; :: thesis: ( not B in { (x /\ S) where x is Element of P : x meets S } or b1 = b2 or b1 misses b2 )
assume B in { (x /\ S) where x is Element of P : x meets S } ; :: thesis: ( b1 = b2 or b1 misses b2 )
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: ( b1 = b2 or b1 misses b2 )
hence ( A = B or A misses B ) by A10, A14; :: thesis: verum
end;
suppose x misses y ; :: thesis: ( b1 = b2 or b1 misses b2 )
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