let X be set ; :: thesis: for a being Element of holds uparrow a = { Y where Y is Subset of : a c= Y }
let a be Element of ; :: thesis: uparrow a = { Y where Y is Subset of : a c= Y }
A1: { Y where Y is Subset of : a c= Y } c= uparrow a

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { Y where Y is Subset of : a c= Y } or x in uparrow a )
assume x in { Y where Y is Subset of : a c= Y } ; :: thesis: x in uparrow a
then consider x' being Subset of such that
A2: x' = x and
A3: a c= x' ;
reconsider x' = x' as Element of by WAYBEL_8:28;
a <= x' by A3, YELLOW_1:2;
hence x in uparrow a by A2, WAYBEL_0:18; :: thesis: verum

end;

uparrow a c= { Y where Y is Subset of : a c= Y }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow a or x in { Y where Y is Subset of : a c= Y } )
assume A4: x in uparrow a ; :: thesis: x in { Y where Y is Subset of : a c= Y }
then reconsider x' = x as Element of ;
a <= x' by A4, WAYBEL_0:18;
then ( x' is Subset of & a c= x ) by WAYBEL_8:28, YELLOW_1:2;
hence x in { Y where Y is Subset of : a c= Y } ; :: thesis: verum

end;

hence uparrow a = { Y where Y is Subset of : a c= Y } by A1, XBOOLE_0:def 10; :: thesis: verum