let R be non empty reflexive transitive RelStr ; :: thesis: for x, y being Element of R holds
( x << y iff uparrow y c= wayabove x )
let x, y be Element of R; :: thesis: ( x << y iff uparrow y c= wayabove x )

hereby :: thesis: ( uparrow y c= wayabove x implies x << y )

assume A1: x << y ; :: thesis: uparrow y c= wayabove x
thus uparrow y c= wayabove x :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in uparrow y or z in wayabove x )
assume A2: z in uparrow y ; :: thesis: z in wayabove x
then reconsider z9 = z as Element of R ;
y <= z9 by A2, WAYBEL_0:18;
then x << z9 by A1, WAYBEL_3:2;
hence z in wayabove x ; :: thesis: verum

end;

end;

y <= y ;
then A3: y in uparrow y by WAYBEL_0:18;
assume uparrow y c= wayabove x ; :: thesis: x << y
hence x << y by A3, WAYBEL_3:8; :: thesis: verum