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