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

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