let L be transitive antisymmetric with_suprema RelStr ; :: thesis: for a, b, c being Element of L st a "\/" b <= c holds
a <= c
let a, b, c be Element of L; :: thesis: ( a "\/" b <= c implies a <= c )
A1: a <= a "\/" b by YELLOW_0:22;
assume a "\/" b <= c ; :: thesis: a <= c
hence a <= c by A1, YELLOW_0:def 2; :: thesis: verum