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 ;
( 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) ) }
;
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;
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))
; verum