let L be transitive antisymmetric RelStr ; :: thesis: for X, Y being set st ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y,L holds
"/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L))
let X, Y be set ; :: thesis: ( ex_inf_of X,L & ex_inf_of Y,L & ex_inf_of X \/ Y,L implies "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) )
assume that
A1: ( ex_inf_of X,L & ex_inf_of Y,L ) and
A2: ex_inf_of X \/ Y,L ; :: thesis: "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L))
set a = "/\" (X,L);
set b = "/\" (Y,L);
set c = "/\" ((X \/ Y),L);
A3: ( "/\" (X,L) is_<=_than X & "/\" (Y,L) is_<=_than Y ) by A1, Th31;

A4: now :: thesis: for d being Element of L st d <= "/\" (X,L) & d <= "/\" (Y,L) holds
"/\" ((X \/ Y),L) >= d

let d be Element of L; :: thesis: ( d <= "/\" (X,L) & d <= "/\" (Y,L) implies "/\" ((X \/ Y),L) >= d )
assume ( d <= "/\" (X,L) & d <= "/\" (Y,L) ) ; :: thesis: "/\" ((X \/ Y),L) >= d
then ( d is_<=_than X & d is_<=_than Y ) by A3, Th4;
then d is_<=_than X \/ Y by Th10;
hence "/\" ((X \/ Y),L) >= d by A2, Th31; :: thesis: verum

end;

( "/\" ((X \/ Y),L) <= "/\" (X,L) & "/\" ((X \/ Y),L) <= "/\" (Y,L) ) by A1, A2, Th35, XBOOLE_1:7;
hence "/\" ((X \/ Y),L) = ("/\" (X,L)) "/\" ("/\" (Y,L)) by A4, Th19; :: thesis: verum