set A = PairSet X;
defpred S₁[ Subset of (PairSet X)] means ex t being set ex l being Subset of X st
( t in X & l in L & $1 = PairSet t,l );
consider F being Subset-Family of (PairSet X) such that
A1: for B being Subset of (PairSet X) holds
( B in F iff S₁[B] ) from SUBSET_1:sch 3();
take F ; :: thesis: for S being set holds
( S in F iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet t,l ) )
let S be set ; :: thesis: ( S in F iff ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet t,l ) )
thus ( S in F implies ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet t,l ) ) by A1; :: thesis: ( ex t being set ex l being Subset of X st
( t in X & l in L & S = PairSet t,l ) implies S in F )
given t being set , l being Subset of X such that A2: ( t in X & l in L & S = PairSet t,l ) ; :: thesis: S in F
S c= PairSet X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in S or a in PairSet X )
assume a in S ; :: thesis: a in PairSet X
then consider y being set such that
A3: ( y in l & a = {t,y} ) by A2, Def9;
thus a in PairSet X by A2, A3, Def8; :: thesis: verum

end;

hence S in F by A1, A2; :: thesis: verum