let L be distributive LATTICE; :: thesis: for p, q, u being Element of L st p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p holds
not u "/\" q <= p
let p, q, u be Element of L; :: thesis: ( p < q & ( for s being Element of L st p < s holds
q <= s ) & not u <= p implies not u "/\" q <= p )
assume that
A1: p < q and
A2: for s being Element of L st p < s holds
q <= s and
A3: not u <= p and
A4: u "/\" q <= p ; :: thesis: contradiction
A5: p <= q by A1, ORDERS_2:def 10;
p = p "\/" (u "/\" q) by A4, YELLOW_0:24
.= (p "\/" u) "/\" (q "\/" p) by WAYBEL_1:6
.= (p "\/" u) "/\" q by A5, YELLOW_0:24
.= q "/\" (q "\/" u) by A1, A2, A3, Th27
.= q by LATTICE3:18 ;
hence contradiction by A1; :: thesis: verum