let L be transitive antisymmetric RelStr ; 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 ; ( 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
; "/\" ((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;
( "/\" ((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; verum