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