let L1, L2 be non empty antisymmetric RelStr ; :: thesis: for D being Subset of [:L1,L2:] st ex_inf_of D,[:L1,L2:] holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]
let D be Subset of [:L1,L2:]; :: thesis: ( ex_inf_of D,[:L1,L2:] implies inf D = [(inf (proj1 D)),(inf (proj2 D))] )
assume A1: ex_inf_of D,[:L1,L2:] ; :: thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
per cases ( D <> {} or D = {} ) ;
suppose D <> {} ; :: thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A1, YELLOW_3:47; :: thesis: verum
end;
suppose A2: D = {} ; :: thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
then ex_inf_of {} ,L2 by A1, FUNCT_5:8, YELLOW_3:42;
then A3: L2 is upper-bounded by Th5;
ex_inf_of {} ,L1 by A1, A2, FUNCT_5:8, YELLOW_3:42;
then L1 is upper-bounded by Th5;
hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A1, A3, YELLOW10:6; :: thesis: verum
end;
end;