let L be non empty RelStr ; for X being set st ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) holds
"/\" (X,L) = "/\" ((X /\ the carrier of L),L)
let X be set ; ( ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) implies "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )
set Y = X /\ the carrier of L;
assume A1:
( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L )
; "/\" (X,L) = "/\" ((X /\ the carrier of L),L)
for x being Element of L holds
( x is_<=_than X iff x is_<=_than X /\ the carrier of L )
by Th5;
hence
"/\" (X,L) = "/\" ((X /\ the carrier of L),L)
by A1, Th49; verum