let L be reflexive antisymmetric with_suprema RelStr ; :: thesis: for a, b being Element of L holds
( a = a "\/" b iff a >= b )
let a, b be Element of L; :: thesis: ( a = a "\/" b iff a >= b )
( a <= a & ( for d being Element of L st d >= a & d >= b holds
a <= d ) ) ;
hence ( a = a "\/" b iff a >= b ) by Th22; :: thesis: verum