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
; 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 ; ( 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; ( 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)
; S in F
S c= PairSet X
hence
S in F
by A1, A2, A3, A4; verum