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