let L be non empty reflexive RelStr ; :: thesis: for x, y being Element of L holds
( x in waybelow y iff x << y )
let x, y be Element of L; :: thesis: ( x in waybelow y iff x << y )
( x in waybelow y iff ex z being Element of L st
( x = z & z << y ) ) ;
hence ( x in waybelow y iff x << y ) ; :: thesis: verum