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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { Y where Y is Subset of X : a c= Y } or x in uparrow a )
assume x in { Y where Y is Subset of X : a c= Y } ; :: thesis: x in uparrow a
then consider x9 being Subset of X such that
A2: x9 = x and
A3: a c= x9 ;
reconsider x9 = x9 as Element of (BoolePoset X) by WAYBEL_8:26;
a <= x9 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 X : a c= Y }

proof

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

end;

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