let S1, S2 be non empty RelStr ; :: thesis: for D being Subset of [:S1,S2:]
for x being Element of S1
for y being Element of S2 holds
( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )
let D be Subset of [:S1,S2:]; :: thesis: for x being Element of S1
for y being Element of S2 holds
( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )
let x be Element of S1; :: thesis: for y being Element of S2 holds
( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )
let y be Element of S2; :: thesis: ( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )
set D1 = proj1 D;
set D2 = proj2 D;
hereby :: thesis: ( x is_<=_than proj1 D & y is_<=_than proj2 D implies [x,y] is_<=_than D )
assume A1: [x,y] is_<=_than D ; :: thesis: ( x is_<=_than proj1 D & y is_<=_than proj2 D )
thus x is_<=_than proj1 D :: thesis: y is_<=_than proj2 D
proof
let q be Element of S1; :: according to LATTICE3:def 8 :: thesis: ( not q in proj1 D or x <= q )
assume q in proj1 D ; :: thesis: x <= q
then consider z being object such that
A2: [q,z] in D by XTUPLE_0:def 12;
reconsider d2 = proj2 D as non empty Subset of S2 by A2, XTUPLE_0:def 13;
reconsider z = z as Element of d2 by A2, XTUPLE_0:def 13;
[x,y] <= [q,z] by A1, A2;
hence x <= q by Th11; :: thesis: verum
end;
thus y is_<=_than proj2 D :: thesis: verum
proof
let q be Element of S2; :: according to LATTICE3:def 8 :: thesis: ( not q in proj2 D or y <= q )
assume q in proj2 D ; :: thesis: y <= q
then consider z being object such that
A3: [z,q] in D by XTUPLE_0:def 13;
reconsider d1 = proj1 D as non empty Subset of S1 by A3, XTUPLE_0:def 12;
reconsider z = z as Element of d1 by A3, XTUPLE_0:def 12;
[x,y] <= [z,q] by A1, A3;
hence y <= q by Th11; :: thesis: verum
end;
end;
assume ( x is_<=_than proj1 D & y is_<=_than proj2 D ) ; :: thesis: [x,y] is_<=_than D
then A4: [x,y] is_<=_than [:(proj1 D),(proj2 D):] by Th33;
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then D c= [:(proj1 D),(proj2 D):] by Th1;
hence [x,y] is_<=_than D by A4; :: thesis: verum