let S, T be non empty antisymmetric upper-bounded RelStr ; :: thesis: for D being Subset of [:S,T:] st ( [:S,T:] is complete or ex_inf_of D,[:S,T:] ) holds
inf D = [(inf (proj1 D)),(inf (proj2 D))]
let D be Subset of [:S,T:]; :: thesis: ( ( [:S,T:] is complete or ex_inf_of D,[:S,T:] ) implies inf D = [(inf (proj1 D)),(inf (proj2 D))] )
assume A1: ( [:S,T:] is complete or ex_inf_of D,[:S,T:] ) ; :: 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 A3: inf (proj2 D) = Top T ;
( inf D = Top [:S,T:] & inf (proj1 D) = Top S ) by A2;
hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A3, Th3; :: thesis: verum

end;

end;