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_inf_of D1,S1 & ex_inf_of D2,S2 holds
inf [:D1,D2:] = [(inf D1),(inf D2)]
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 holds
inf [:D1,D2:] = [(inf D1),(inf D2)]
let D2 be non empty Subset of S2; :: thesis: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 implies inf [:D1,D2:] = [(inf D1),(inf D2)] )
assume A1: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) ; :: thesis: inf [:D1,D2:] = [(inf D1),(inf D2)]
set s = inf [:D1,D2:];
inf [: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 & inf [: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_inf_of [:D1,D2:],[:S1,S2:] by A1, Th40;
then A4: [s1,s2] is_<=_than [:D1,D2:] by A2, YELLOW_0:31;
then A5: s1 is_<=_than D1 by Th32;
A6: for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[s1,s2] >= b by A2, A3, YELLOW_0:31;
then for b being Element of S1 st b is_<=_than D1 holds
s1 >= b by A1, Th36;
then A7: s1 = inf D1 by A5, YELLOW_0:31;
A8: s2 is_<=_than D2 by A4, Th32;
for b being Element of S2 st b is_<=_than D2 holds
s2 >= b by A1, A6, Th36;
hence inf [:D1,D2:] = [(inf D1),(inf D2)] by A2, A7, A8, YELLOW_0:31; :: thesis: verum