hereby :: according to WAYBEL_0:def 20 :: thesis: verum
let z, y be Element of L; :: thesis: ( z in wayabove x & y >= z implies y in wayabove x )
assume z in wayabove x ; :: thesis: ( y >= z implies y in wayabove x )
then z >> x by Th8;
then ( y >= z implies y >> x ) by Th2;
hence ( y >= z implies y in wayabove x ) ; :: thesis: verum
end;