set C = { y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } ;
for x being object st x in { y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } holds
x in [#] (A ~ p)

proof

let x be object ; :: thesis: ( x in { y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } implies x in [#] (A ~ p) )
assume x in { y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } ; :: thesis: x in [#] (A ~ p)
then consider y1 being Element of (A ~ p) such that
A2: y1 = x and
ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y1 = Class ((EqRel (Loc (A,p))),a) ) ;
thus x in [#] (A ~ p) by A2; :: thesis: verum

end;

then { y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } c= [#] (A ~ p) ;
hence { y where y is Element of (A ~ p) : ex a being Element of Frac (Loc (A,p)) st
( a in [:p,(Loc (A,p)):] & y = Class ((EqRel (Loc (A,p))),a) ) } is Subset of ([#] (A ~ p)) ; :: thesis: verum