let it1, it2 be Subset of the carrier' of G; :: thesis: ( ( for e being set holds
( e in it1 iff ( e in the carrier' of G & e in X & the Source of G . e = v ) ) ) & ( for e being set holds
( e in it2 iff ( e in the carrier' of G & e in X & the Source of G . e = v ) ) ) implies it1 = it2 )
assume that
A5: for e being set holds
( e in it1 iff ( e in the carrier' of G & e in X & the Source of G . e = v ) ) and
A6: for e being set holds
( e in it2 iff ( e in the carrier' of G & e in X & the Source of G . e = v ) ) ; :: thesis: it1 = it2

now :: thesis: for e being object holds
( e in it1 iff e in it2 )

let e be object ; :: thesis: ( e in it1 iff e in it2 )
( e in it1 iff ( e in the carrier' of G & e in X & the Source of G . e = v ) ) by A5;
hence ( e in it1 iff e in it2 ) by A6; :: thesis: verum

end;

hence it1 = it2 by TARSKI:2; :: thesis: verum