let L be non empty reflexive antisymmetric RelStr ; :: thesis: for x being Element of L holds
( waybelow x c= downarrow x & wayabove x c= uparrow x )
let x be Element of L; :: thesis: ( waybelow x c= downarrow x & wayabove x c= uparrow x )
hereby :: according to TARSKI:def 3 :: thesis: wayabove x c= uparrow x
let a be object ; :: thesis: ( a in waybelow x implies a in downarrow x )
assume a in waybelow x ; :: thesis: a in downarrow x
then consider y being Element of L such that
A1: a = y and
A2: y << x ;
y <= x by A2, Th1;
hence a in downarrow x by A1, WAYBEL_0:17; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in wayabove x or a in uparrow x )
assume a in wayabove x ; :: thesis: a in uparrow x
then consider y being Element of L such that
A3: a = y and
A4: y >> x ;
x <= y by A4, Th1;
hence a in uparrow x by A3, WAYBEL_0:18; :: thesis: verum