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

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