let S1, S2 be non empty antisymmetric RelStr ; :: thesis: for D being Subset of [:S1,S2:] holds
( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] )
let D be Subset of [:S1,S2:]; :: thesis: ( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[:S1,S2:] )
A1: the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then A2: D c= [:(proj1 D),(proj2 D):] by Th1;
hereby :: thesis: ( ex_sup_of D,[:S1,S2:] implies ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) )
assume that
A3: ex_sup_of proj1 D,S1 and
A4: ex_sup_of proj2 D,S2 ; :: thesis: ex_sup_of D,[:S1,S2:]
ex a being Element of [:S1,S2:] st
( D is_<=_than a & ( for b being Element of [:S1,S2:] st D is_<=_than b holds
a <= b ) )
proof
consider x2 being Element of S2 such that
A5: proj2 D is_<=_than x2 and
A6: for b being Element of S2 st proj2 D is_<=_than b holds
x2 <= b by A4, YELLOW_0:15;
consider x1 being Element of S1 such that
A7: proj1 D is_<=_than x1 and
A8: for b being Element of S1 st proj1 D is_<=_than b holds
x1 <= b by A3, YELLOW_0:15;
take a = [x1,x2]; :: thesis: ( D is_<=_than a & ( for b being Element of [:S1,S2:] st D is_<=_than b holds
a <= b ) )
thus D is_<=_than a :: thesis: for b being Element of [:S1,S2:] st D is_<=_than b holds
a <= b
proof
let q be Element of [:S1,S2:]; :: according to LATTICE3:def 9 :: thesis: ( not q in D or q <= a )
assume q in D ; :: thesis: q <= a
then consider q1, q2 being object such that
A9: q1 in proj1 D and
A10: q2 in proj2 D and
A11: q = [q1,q2] by A2, ZFMISC_1:def 2;
reconsider q2 = q2 as Element of S2 by A10;
reconsider q1 = q1 as Element of S1 by A9;
( q1 <= x1 & q2 <= x2 ) by A7, A5, A9, A10;
hence q <= a by A11, Th11; :: thesis: verum
end;
let b be Element of [:S1,S2:]; :: thesis: ( D is_<=_than b implies a <= b )
assume A12: D is_<=_than b ; :: thesis: a <= b
A13: b = [(b `1),(b `2)] by A1, MCART_1:21;
then proj2 D is_<=_than b `2 by A12, Th31;
then A14: x2 <= b `2 by A6;
proj1 D is_<=_than b `1 by A12, A13, Th31;
then x1 <= b `1 by A8;
hence a <= b by A13, A14, Th11; :: thesis: verum
end;
hence ex_sup_of D,[:S1,S2:] by YELLOW_0:15; :: thesis: verum
end;
assume ex_sup_of D,[:S1,S2:] ; :: thesis: ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 )
then consider x being Element of [:S1,S2:] such that
A15: D is_<=_than x and
A16: for b being Element of [:S1,S2:] st D is_<=_than b holds
x <= b by YELLOW_0:15;
A17: x = [(x `1),(x `2)] by A1, MCART_1:21;
then A18: proj1 D is_<=_than x `1 by A15, Th31;
A19: proj2 D is_<=_than x `2 by A15, A17, Th31;
for b being Element of S1 st proj1 D is_<=_than b holds
x `1 <= b
proof
let b be Element of S1; :: thesis: ( proj1 D is_<=_than b implies x `1 <= b )
assume proj1 D is_<=_than b ; :: thesis: x `1 <= b
then D is_<=_than [b,(x `2)] by A19, Th31;
then x <= [b,(x `2)] by A16;
hence x `1 <= b by A17, Th11; :: thesis: verum
end;
hence ex_sup_of proj1 D,S1 by A18, YELLOW_0:15; :: thesis: ex_sup_of proj2 D,S2
for b being Element of S2 st proj2 D is_<=_than b holds
x `2 <= b
proof
let b be Element of S2; :: thesis: ( proj2 D is_<=_than b implies x `2 <= b )
assume proj2 D is_<=_than b ; :: thesis: x `2 <= b
then D is_<=_than [(x `1),b] by A18, Th31;
then x <= [(x `1),b] by A16;
hence x `2 <= b by A17, Th11; :: thesis: verum
end;
hence ex_sup_of proj2 D,S2 by A19, YELLOW_0:15; :: thesis: verum