let L be transitive antisymmetric with_suprema RelStr ; :: 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
p "\/" u = q "\/" u
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 p "\/" u = q "\/" u )
assume that
A1: p < q and
A2: for s being Element of L st p < s holds
q <= s and
A3: not u <= p ; :: thesis: p "\/" u = q "\/" u
A4: q "\/" u >= q by YELLOW_0:22;
A5: now :: thesis: for v being Element of L st v >= p & v >= u holds
q "\/" u <= v
let v be Element of L; :: thesis: ( v >= p & v >= u implies q "\/" u <= v )
assume that
A6: v >= p and
A7: v >= u ; :: thesis: q "\/" u <= v
v > p by A3, A6, A7, ORDERS_2:def 6;
then v >= q by A2;
hence q "\/" u <= v by A7, YELLOW_0:22; :: thesis: verum
end;
p <= q by A1, ORDERS_2:def 6;
then A8: q "\/" u >= p by A4, ORDERS_2:3;
q "\/" u >= u by YELLOW_0:22;
hence p "\/" u = q "\/" u by A8, A5, YELLOW_0:22; :: thesis: verum