let x, y be Element of (L ~ ); :: according to WAYBEL_0:def 29 :: thesis: ( x <= y or y <= x )
A1: ( ~ x = x & ~ y = y & (~ x) ~ = ~ x & (~ y) ~ = ~ y ) ;
( ~ x <= ~ y or ~ x >= ~ y ) by Def29;
hence ( x <= y or y <= x ) by A1, LATTICE3:9; :: thesis: verum