let X be non empty set ; :: thesis: for Y being set st Y c= X holds
for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
let Y be set ; :: thesis: ( Y c= X implies for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y )
assume A1: Y c= X ; :: thesis: for P being a_partition of X holds { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
let P be a_partition of X; :: thesis: { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y
set Q = { (a /\ Y) where a is Element of P : a meets Y } ;
{ (a /\ Y) where a is Element of P : a meets Y } c= bool Y
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (a /\ Y) where a is Element of P : a meets Y } or x in bool Y )
reconsider xx = x as set by TARSKI:1;
assume x in { (a /\ Y) where a is Element of P : a meets Y } ; :: thesis: x in bool Y
then ex p being Element of P st
( x = p /\ Y & p meets Y ) ;
then A2: xx c= X /\ Y by XBOOLE_1:26;
X /\ Y = Y by A1, XBOOLE_1:28;
hence x in bool Y by A2; :: thesis: verum
end;
then reconsider Q = { (a /\ Y) where a is Element of P : a meets Y } as Subset-Family of Y ;
Q is a_partition of Y
proof
thus union Q c= Y ; :: according to XBOOLE_0:def 10,EQREL_1:def 4 :: thesis: ( Y c= union Q & ( for b1 being Element of bool Y holds
( not b1 in Q or ( not b1 = {} & ( for b2 being Element of bool Y holds
( not b2 in Q or b1 = b2 or b1 misses b2 ) ) ) ) ) )
thus Y c= union Q :: thesis: for b1 being Element of bool Y holds
( not b1 in Q or ( not b1 = {} & ( for b2 being Element of bool Y holds
( not b2 in Q or b1 = b2 or b1 misses b2 ) ) ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in union Q )
assume A3: x in Y ; :: thesis: x in union Q
X = union P by EQREL_1:def 4;
then consider p being set such that
A4: x in p and
A5: p in P by A1, A3, TARSKI:def 4;
A6: p meets Y by A3, A4, XBOOLE_0:3;
A7: x in p /\ Y by A3, A4, XBOOLE_0:def 4;
p /\ Y in Q by A5, A6;
hence x in union Q by A7, TARSKI:def 4; :: thesis: verum
end;
let A be Subset of Y; :: thesis: ( not A in Q or ( not A = {} & ( for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 ) ) ) )
assume A in Q ; :: thesis: ( not A = {} & ( for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 ) ) )
then consider p being Element of P such that
A8: A = p /\ Y and
A9: p meets Y ;
thus A <> {} by A8, A9; :: thesis: for b1 being Element of bool Y holds
( not b1 in Q or A = b1 or A misses b1 )
let B be Subset of Y; :: thesis: ( not B in Q or A = B or A misses B )
assume B in Q ; :: thesis: ( A = B or A misses B )
then consider p1 being Element of P such that
A10: B = p1 /\ Y and
p1 meets Y ;
assume A <> B ; :: thesis: A misses B
then p misses p1 by A8, A10, EQREL_1:def 4;
then A misses p1 by A8, XBOOLE_1:74;
hence A misses B by A10, XBOOLE_1:74; :: thesis: verum
end;
hence { (a /\ Y) where a is Element of P : a meets Y } is a_partition of Y ; :: thesis: verum