let S1, S2 be non empty antisymmetric RelStr ; 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; 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; ( 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 )
; 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 object such that
A2:
s1 in the carrier of S1
and
A3:
s2 in the carrier of S2
and
A4:
inf [: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_inf_of [:D1,D2:],[:S1,S2:]
by A1, Th40;
then A6:
[s1,s2] is_<=_than [:D1,D2:]
by A4, YELLOW_0:31;
then A7:
s1 is_<=_than D1
by Th32;
A8:
for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds
[s1,s2] >= b
by A4, A5, YELLOW_0:31;
then
for b being Element of S1 st b is_<=_than D1 holds
s1 >= b
by A1, Th36;
then A9:
s1 = inf D1
by A7, YELLOW_0:31;
A10:
s2 is_<=_than D2
by A6, Th32;
for b being Element of S2 st b is_<=_than D2 holds
s2 >= b
by A1, A8, Th36;
hence
inf [:D1,D2:] = [(inf D1),(inf D2)]
by A4, A9, A10, YELLOW_0:31; verum