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

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

uparrow a c= { Y where Y is Subset of X : a c= Y }
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;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

proof

hence
uparrow a = { Y where Y is Subset of X : a c= Y }
by A1, XBOOLE_0:def 10; :: thesis: verum
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;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