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 ) & not u <= p ) and
A3: u "/\" q <= p ; :: thesis: contradiction
A4: p <= q by A1, ORDERS_2:def 6;
p = p "\/" (u "/\" q) by A3, YELLOW_0:24
.= (p "\/" u) "/\" (q "\/" p) by WAYBEL_1:5
.= (p "\/" u) "/\" q by A4, YELLOW_0:24
.= q "/\" (q "\/" u) by A1, A2, Th27
.= q by LATTICE3:18 ;
hence contradiction by A1; :: thesis: verum