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) )
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 A2: (x "/\" ) . (inf X) is_<=_than (x "/\" ) .: X by YELLOW_2:15;
for b being Element of N st b is_<=_than (x "/\" ) .: X holds
(x "/\" ) . (inf X) >= b

proof

let b be Element of N; :: thesis: ( b is_<=_than (x "/\" ) .: X implies (x "/\" ) . (inf X) >= b )
assume A3: b is_<=_than (x "/\" ) .: X ; :: thesis: (x "/\" ) . (inf X) >= b
consider y being set such that
A4: y in X by XBOOLE_0:def 1;
reconsider y = y as Element of N by A4;
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 A4;
then A6: b <= x "/\" y by A3, LATTICE3:def 8;
x "/\" y <= x by YELLOW_0:23;
then A7: b <= x by A6, ORDERS_2:26;
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 A8: b <= x "/\" c by A3, LATTICE3:def 8;
x "/\" c <= c by YELLOW_0:23;
hence b <= c by A8, ORDERS_2:26; :: thesis: verum

end;

then b <= inf X by A1, YELLOW_0:def 10;
then b "/\" b <= x "/\" (inf X) by A7, 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;

hence inf ((x "/\" ) .: X) = (x "/\" ) . (inf X) by A2, YELLOW_0:33; :: thesis: verum