let N be non empty complete Poset; :: thesis: for x being Element of N holds x "/\" is meet-preserving
let x be Element of N; :: thesis: x "/\" is meet-preserving
let a, b be Element of N; :: according to WAYBEL_0:def 34 :: thesis: x "/\" preserves_inf_of {a,b}
thus x "/\" preserves_inf_of {a,b} by Th11; :: thesis: verum