let L be non empty RelStr ; :: thesis: ( ( for A being Subset of L holds ex_inf_of A,L ) implies for X being set holds
( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) )
assume A1: for A being Subset of L holds ex_inf_of A,L ; :: thesis: for X being set holds
( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )
let X be set ; :: thesis: ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )
set Y = X /\ the carrier of L;
set a = "/\" ((X /\ the carrier of L),L);
reconsider Y = X /\ the carrier of L as Subset of L by XBOOLE_1:17;
A2: ex_inf_of Y,L by A1;
A3: "/\" ((X /\ the carrier of L),L) is_<=_than X

proof

let x be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not x in X or "/\" ((X /\ the carrier of L),L) <= x )
assume x in X ; :: thesis: "/\" ((X /\ the carrier of L),L) <= x
then A4: x in Y by XBOOLE_0:def 4;
"/\" ((X /\ the carrier of L),L) is_<=_than Y by A2, YELLOW_0:def 10;
hence "/\" ((X /\ the carrier of L),L) <= x by A4; :: thesis: verum

end;

A5: for b being Element of L st b is_<=_than X holds
b <= "/\" ((X /\ the carrier of L),L)

proof

let b be Element of L; :: thesis: ( b is_<=_than X implies b <= "/\" ((X /\ the carrier of L),L) )
A6: Y c= X by XBOOLE_1:17;
assume b is_<=_than X ; :: thesis: b <= "/\" ((X /\ the carrier of L),L)
then b is_<=_than Y by A6;
hence b <= "/\" ((X /\ the carrier of L),L) by A2, YELLOW_0:def 10; :: thesis: verum

end;

ex_inf_of X,L by A2, YELLOW_0:50;
hence ( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) ) by A3, A5, YELLOW_0:def 10; :: thesis: verum