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 object 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:61;
then x "/\" y in (x "/\") .: X by A3;
then A6: b <= x "/\" y by A4;
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;
x "/\" c <= c by YELLOW_0:23;
hence b <= c by A7, ORDERS_2:3; :: 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:3;
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:13;
hence "/\" (((x "/\") .: X),N) = (x "/\") . ("/\" (X,N)) by A2, YELLOW_0:33; :: thesis: verum