let N be non empty complete Poset; :: thesis: for x being Element of N
for X being non empty Subset of N holds x "/\" preserves_inf_of X
let x be Element of N; :: thesis: for X being non empty Subset of N holds x "/\" preserves_inf_of X
let X be non empty Subset of N; :: thesis: x "/\" preserves_inf_of X
assume A1: ex_inf_of X,N ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (x "/\" ) .: X,N & "/\" ((x "/\" ) .: X),N = (x "/\" ) . ("/\" X,N) )
A2: for b being Element of N st b is_<=_than (x "/\" ) .: X holds
(x "/\" ) . (inf X) >= b

proof

consider y being set such that
A3: y in X by XBOOLE_0:def 1;
reconsider y = y as Element of N by A3;
let b be Element of N; :: thesis: ( b is_<=_than (x "/\" ) .: X implies (x "/\" ) . (inf X) >= b )
assume A4: b is_<=_than (x "/\" ) .: X ; :: thesis: (x "/\" ) . (inf X) >= b
A5: (x "/\" ) .: X = { (x "/\" z) where z is Element of N : z in X } by WAYBEL_1:64;
then x "/\" y in (x "/\" ) .: X by A3;
then A6: b <= x "/\" y by A4, LATTICE3:def 8;
X is_>=_than b

proof

let c be Element of N; :: according to LATTICE3:def 8 :: thesis: ( not c in X or b <= c )
assume c in X ; :: thesis: b <= c
then x "/\" c in (x "/\" ) .: X by A5;
then A7: b <= x "/\" c by A4, LATTICE3:def 8;
x "/\" c <= c by YELLOW_0:23;
hence b <= c by A7, ORDERS_2:26; :: thesis: verum

end;

then A8: b <= inf X by A1, YELLOW_0:def 10;
x "/\" y <= x by YELLOW_0:23;
then b <= x by A6, ORDERS_2:26;
then b "/\" b <= x "/\" (inf X) by A8, YELLOW_3:2;
then b <= x "/\" (inf X) by YELLOW_0:25;
hence b <= (x "/\" ) . (inf X) by WAYBEL_1:def 18; :: thesis: verum

end;

thus ex_inf_of (x "/\" ) .: X,N by YELLOW_0:17; :: thesis: "/\" ((x "/\" ) .: X),N = (x "/\" ) . ("/\" X,N)
inf X is_<=_than X by A1, YELLOW_0:def 10;
then (x "/\" ) . (inf X) is_<=_than (x "/\" ) .: X by YELLOW_2:15;
hence "/\" ((x "/\" ) .: X),N = (x "/\" ) . ("/\" X,N) by A2, YELLOW_0:33; :: thesis: verum