let L be non empty reflexive antisymmetric RelStr ; :: thesis: for x being Element of L holds x is_<=_than wayabove x
let x, y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in wayabove x or x <= y )
assume y in wayabove x ; :: thesis: x <= y
then y >> x by Th8;
hence x <= y by Th1; :: thesis: verum