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

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