let S1, S2 be non empty antisymmetric RelStr ; :: thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 holds
sup [:D1,D2:] = [(sup D1),(sup D2)]
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 holds
sup [:D1,D2:] = [(sup D1),(sup D2)]
let D2 be non empty Subset of S2; :: thesis: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 implies sup [:D1,D2:] = [(sup D1),(sup D2)] )
assume A1: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) ; :: thesis: sup [:D1,D2:] = [(sup D1),(sup D2)]
set s = sup [:D1,D2:];
sup [:D1,D2:] is Element of [: the carrier of S1, the carrier of S2:] by Def2;
then consider s1, s2 being object such that
A2: s1 in the carrier of S1 and
A3: s2 in the carrier of S2 and
A4: sup [:D1,D2:] = [s1,s2] by ZFMISC_1:def 2;
reconsider s2 = s2 as Element of S2 by A3;
reconsider s1 = s1 as Element of S1 by A2;
A5: ex_sup_of [:D1,D2:],[:S1,S2:] by A1, Th39;
then A6: [s1,s2] is_>=_than [:D1,D2:] by A4, YELLOW_0:30;
then A7: s1 is_>=_than D1 by Th29;
A8: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[s1,s2] <= b by A4, A5, YELLOW_0:30;
then for b being Element of S1 st b is_>=_than D1 holds
s1 <= b by A1, Th35;
then A9: s1 = sup D1 by A7, YELLOW_0:30;
A10: s2 is_>=_than D2 by A6, Th29;
for b being Element of S2 st b is_>=_than D2 holds
s2 <= b by A1, A8, Th35;
hence sup [:D1,D2:] = [(sup D1),(sup D2)] by A4, A9, A10, YELLOW_0:30; :: thesis: verum