set A = PairSet X;
defpred S1[ 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 S1[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 and
A3: l in L and
A4: S = PairSet (t,l) ; :: thesis: S in F
S c= PairSet X
proof
let a be object ; :: 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 ex y being set st
( y in l & a = {t,y} ) by A4, Def9;
hence a in PairSet X by A2, Def8; :: thesis: verum
end;
hence S in F by A1, A2, A3, A4; :: thesis: verum