let X, Y be non empty set ; :: thesis: for P being a_partition of X
for Q being a_partition of Y holds { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:]
let P be a_partition of X; :: thesis: for Q being a_partition of Y holds { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:]
let Q be a_partition of Y; :: thesis: { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:]
set PQ = { [:p,q:] where p is Element of P, q is Element of Q : verum } ;
{ [:p,q:] where p is Element of P, q is Element of Q : verum } c= bool [:X,Y:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [:p,q:] where p is Element of P, q is Element of Q : verum } or x in bool [:X,Y:] )
assume x in { [:p,q:] where p is Element of P, q is Element of Q : verum } ; :: thesis: x in bool [:X,Y:]
then ex p being Element of P ex q being Element of Q st x = [:p,q:] ;
hence x in bool [:X,Y:] ; :: thesis: verum

end;

then reconsider PQ = { [:p,q:] where p is Element of P, q is Element of Q : verum } as Subset-Family of [:X,Y:] ;
PQ is a_partition of [:X,Y:]

proof

thus union PQ = [:X,Y:] :: according to EQREL_1:def 4 :: thesis: for b₁ being Element of bool [:X,Y:] holds
( not b₁ in PQ or ( not b₁ = {} & ( for b₂ being Element of bool [:X,Y:] holds
( not b₂ in PQ or b₁ = b₂ or b₁ misses b₂ ) ) ) )

proof

let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in union PQ or [x,y] in [:X,Y:] ) & ( not [x,y] in [:X,Y:] or [x,y] in union PQ ) )
thus ( [x,y] in union PQ implies [x,y] in [:X,Y:] ) ; :: thesis: ( not [x,y] in [:X,Y:] or [x,y] in union PQ )
assume A1: [x,y] in [:X,Y:] ; :: thesis: [x,y] in union PQ
then A2: x in X by ZFMISC_1:87;
A3: y in Y by A1, ZFMISC_1:87;
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 A2, TARSKI:def 4;
Y = union Q by EQREL_1:def 4;
then consider q being set such that
A6: y in q and
A7: q in Q by A3, TARSKI:def 4;
A8: [x,y] in [:p,q:] by A4, A6, ZFMISC_1:87;
[:p,q:] in PQ by A5, A7;
hence [x,y] in union PQ by A8, TARSKI:def 4; :: thesis: verum

end;

let A be Subset of [:X,Y:]; :: thesis: ( not A in PQ or ( not A = {} & ( for b₁ being Element of bool [:X,Y:] holds
( not b₁ in PQ or A = b₁ or A misses b₁ ) ) ) )
assume A in PQ ; :: thesis: ( not A = {} & ( for b₁ being Element of bool [:X,Y:] holds
( not b₁ in PQ or A = b₁ or A misses b₁ ) ) )
then consider p being Element of P, q being Element of Q such that
A9: A = [:p,q:] ;
thus A <> {} by A9; :: thesis: for b₁ being Element of bool [:X,Y:] holds
( not b₁ in PQ or A = b₁ or A misses b₁ )
let B be Subset of [:X,Y:]; :: thesis: ( not B in PQ or A = B or A misses B )
assume B in PQ ; :: thesis: ( A = B or A misses B )
then consider p1 being Element of P, q1 being Element of Q such that
A10: B = [:p1,q1:] ;
assume A <> B ; :: thesis: A misses B
then ( p <> p1 or q <> q1 ) by A9, A10;
then ( p misses p1 or q misses q1 ) by EQREL_1:def 4;
then ( p /\ p1 = {} or q /\ q1 = {} ) ;
then ( A /\ B = [:{},(q /\ q1):] or A /\ B = [:(p /\ p1),{}:] ) by A9, A10, ZFMISC_1:100;
then A /\ B = {} ;
hence A misses B ; :: thesis: verum

end;

hence { [:p,q:] where p is Element of P, q is Element of Q : verum } is a_partition of [:X,Y:] ; :: thesis: verum