let L be non empty reflexive transitive RelStr ; :: thesis: for x, y being Element of L st x <= y holds
( waybelow x c= waybelow y & wayabove y c= wayabove x )
let x, y be Element of L; :: thesis: ( x <= y implies ( waybelow x c= waybelow y & wayabove y c= wayabove x ) )
assume A1: x <= y ; :: thesis: ( waybelow x c= waybelow y & wayabove y c= wayabove x )
hereby :: according to TARSKI:def 3 :: thesis: wayabove y c= wayabove x
let z be object ; :: thesis: ( z in waybelow x implies z in waybelow y )
assume z in waybelow x ; :: thesis: z in waybelow y
then consider v being Element of L such that
A2: z = v and
A3: v << x ;
v << y by A1, A3, Th2;
hence z in waybelow y by A2; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in wayabove y or z in wayabove x )
assume z in wayabove y ; :: thesis: z in wayabove x
then consider v being Element of L such that
A4: z = v and
A5: v >> y ;
v >> x by A1, A5, Th2;
hence z in wayabove x by A4; :: thesis: verum