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

hereby :: thesis: ( downarrow x c= waybelow y implies x << y )

assume A1: x << y ; :: thesis: downarrow x c= waybelow y
thus downarrow x c= waybelow y :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in downarrow x or z in waybelow y )
assume A2: z in downarrow x ; :: thesis: z in waybelow y
then reconsider z' = z as Element of R ;
z' <= x by A2, WAYBEL_0:17;
then z' << y by A1, WAYBEL_3:2;
hence z in waybelow y ; :: thesis: verum

end;

end;

assume A3: downarrow x c= waybelow y ; :: thesis: x << y
x <= x ;
then x in downarrow x by WAYBEL_0:17;
hence x << y by A3, WAYBEL_3:7; :: thesis: verum