take F = uparrow (Top L); :: thesis: F is proper
assume not F is proper ; :: thesis: contradiction
then A1: F = the carrier of L ;
now :: thesis: for x, y being Element of L holds x = y
let x, y be Element of L; :: thesis: x = y
A2: F = {(Top L)} by WAYBEL_4:24;
then x = Top L by A1, TARSKI:def 1;
hence x = y by A1, A2, TARSKI:def 1; :: thesis: verum
end;
hence contradiction by STRUCT_0:def 10; :: thesis: verum