let X be set ; :: thesis: for A, B being Subset of X holds {A,B} is N_Sub_set_fam of X
let A, B be Subset of X; :: thesis: {A,B} is N_Sub_set_fam of X
ex F being sequence of (bool X) st
( rng F = {A,B} & F . 0 = A & ( for n being Nat st 0 < n holds
F . n = B ) ) by Th19;
hence {A,B} is N_Sub_set_fam of X by SUPINF_2:def 8; :: thesis: verum