let L be complete LATTICE; :: thesis: for x being Element of L holds
( uparrow x is Open Filter of L iff x is compact )
let x be Element of L; :: thesis: ( uparrow x is Open Filter of L iff x is compact )
thus ( uparrow x is Open Filter of L implies x is compact ) :: thesis: ( x is compact implies uparrow x is Open Filter of L )

proof

x <= x ;
then A1: x in uparrow x by WAYBEL_0:18;
assume uparrow x is Open Filter of L ; :: thesis: x is compact
then consider y being Element of L such that
A2: y in uparrow x and
A3: y << x by A1, WAYBEL_6:def 1;
x <= y by A2, WAYBEL_0:18;
then x << x by A3, WAYBEL_3:2;
hence x is compact by WAYBEL_3:def 2; :: thesis: verum

end;

assume A4: x is compact ; :: thesis: uparrow x is Open Filter of L

now :: thesis: for u being Element of L st u in uparrow x holds
ex x2 being Element of L st
( x2 in uparrow x & x2 << u )

let u be Element of L; :: thesis: ( u in uparrow x implies ex x2 being Element of L st
( x2 in uparrow x & x2 << u ) )
assume u in uparrow x ; :: thesis: ex x2 being Element of L st
( x2 in uparrow x & x2 << u )
then A5: x <= u by WAYBEL_0:18;
take x2 = x; :: thesis: ( x2 in uparrow x & x2 << u )
x <= x2 ;
hence x2 in uparrow x by WAYBEL_0:18; :: thesis: x2 << u
x << x by A4, WAYBEL_3:def 2;
hence x2 << u by A5, WAYBEL_3:2; :: thesis: verum

end;

hence uparrow x is Open Filter of L by WAYBEL_6:def 1; :: thesis: verum