let X be set ; :: thesis: for a being Element of () holds uparrow a = { Y where Y is Subset of X : a c= Y }
let a be Element of (); :: 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:
then consider x9 being Subset of X such that
A2: x9 = x and
A3: a c= x9 ;
reconsider x9 = x9 as Element of () by WAYBEL_8:26;
a <= x9 by ;
hence x in uparrow a by ; :: 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 () ;
a <= x9 by ;
then ( x9 is Subset of X & a c= x9 ) by ;
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 ; :: thesis: verum