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