let L be non empty RelStr ; :: thesis: 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 ; :: thesis: ( ( 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 ( ex_inf_of X,L or ex_inf_of X /\ the carrier of L,L ) ; :: thesis: "/\" X,L = "/\" (X /\ the carrier of L),L
then ( ex_inf_of X,L & ( for x being Element of L holds
( x is_<=_than X iff x is_<=_than X /\ the carrier of L ) ) ) by Th5, Th50;
hence "/\" X,L = "/\" (X /\ the carrier of L),L by Th49; :: thesis: verum