now :: thesis: for x, y being Element of L st x in {(Top L)} & x <= y holds
y in {(Top L)}
let x, y be Element of L; :: thesis: ( x in {(Top L)} & x <= y implies y in {(Top L)} )
assume that
A1: x in {(Top L)} and
A2: x <= y ; :: thesis: y in {(Top L)}
x = Top L by A1, TARSKI:def 1;
then y = Top L by A2, WAYBEL15:3;
hence y in {(Top L)} by TARSKI:def 1; :: thesis: verum
end;
then {(Top L)} is Filter of L by WAYBEL_0:5, WAYBEL_0:def 20;
then {(Top L)} in { Y where Y is Filter of L : verum } ;
hence not Filt L is empty by WAYBEL_0:def 24; :: thesis: verum