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 set ; :: 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 consider p being Element of P, q being Element of Q such that
A1: x = [:p,q:] ;
thus x in bool [:X,Y:] by A1; :: 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 6 :: 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 set ; :: 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 [x,y] in [:X,Y:] ; :: thesis: [x,y] in union PQ
then A2: ( x in X & y in Y ) by ZFMISC_1:106;
X = union P by EQREL_1:def 6;
then consider p being set such that
A3: ( x in p & p in P ) by A2, TARSKI:def 4;
Y = union Q by EQREL_1:def 6;
then consider q being set such that
A4: ( y in q & q in Q ) by A2, TARSKI:def 4;
( [x,y] in [:p,q:] & [:p,q:] in PQ ) by A3, A4, ZFMISC_1:106;
hence [x,y] in union PQ by 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
A5: A = [:p,q:] ;
thus A <> {} by A5; :: 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
A6: B = [:p1,q1:] ;
assume A <> B ; :: thesis: A misses B
then ( p <> p1 or q <> q1 ) by A5, A6;
then ( p misses p1 or q misses q1 ) by EQREL_1:def 6;
then ( p /\ p1 = {} or q /\ q1 = {} ) by XBOOLE_0:def 7;
then ( A /\ B = [:{} ,(q /\ q1):] or A /\ B = [:(p /\ p1),{} :] ) by A5, A6, ZFMISC_1:123;
then A /\ B = {} by ZFMISC_1:113;
hence A misses B by XBOOLE_0:def 7; :: 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