let L be sup-Semilattice; :: thesis: for a, b, c being Element of L st a <= c & b <= c holds
a "\/" b <= c
let a, b, c be Element of L; :: thesis: ( a <= c & b <= c implies a "\/" b <= c )
assume that
A1: a <= c and
A2: b <= c ; :: thesis: a "\/" b <= c
c "\/" b = c by A2, Th8;
hence a "\/" b <= c by A1, Th7; :: thesis: verum