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;
then A3: ex_inf_of X,L by YELLOW_0:50;
A4: "/\" (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 A5: 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 A5, LATTICE3:def 8; :: thesis: verum

end;

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 )
assume A6: b is_<=_than X ; :: thesis: b <= "/\" (X /\ the carrier of L),L
Y c= X by XBOOLE_1:17;
then b is_<=_than Y by A6, YELLOW_0:9;
hence b <= "/\" (X /\ the carrier of L),L by A2, YELLOW_0:def 10; :: thesis: verum

end;

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