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 set such that
A2: ( s1 in the carrier of S1 & s2 in the carrier of S2 & sup [:D1,D2:] = [s1,s2] ) by ZFMISC_1:def 2;
reconsider s1 = s1 as Element of S1 by A2;
reconsider s2 = s2 as Element of S2 by A2;
A3: ex_sup_of [:D1,D2:],[:S1,S2:] by A1, Th39;
then A4: [s1,s2] is_>=_than [:D1,D2:] by A2, YELLOW_0:30;
then A5: s1 is_>=_than D1 by Th29;
A6: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[s1,s2] <= b by A2, A3, YELLOW_0:30;
then for b being Element of S1 st b is_>=_than D1 holds
s1 <= b by A1, Th35;
then A7: s1 = sup D1 by A5, YELLOW_0:30;
A8: s2 is_>=_than D2 by A4, Th29;
for b being Element of S2 st b is_>=_than D2 holds
s2 <= b by A1, A6, Th35;
hence sup [:D1,D2:] = [(sup D1),(sup D2)] by A2, A7, A8, YELLOW_0:30; :: thesis: verum