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 object ; :: 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 z9 = z as Element of R ;
z9 <= x by A2, WAYBEL_0:17;
then z9 << y by A1, WAYBEL_3:2;
hence z in waybelow y ; :: thesis: verum

end;

end;

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