let X be set ; :: thesis: for A, B being Subset of holds {A,B,{} } is N_Sub_set_fam of X
let A, B be Subset of ; :: thesis: {A,B,{} } is N_Sub_set_fam of X
{} is Subset of by XBOOLE_1:2;
then consider C being Subset of such that
A1: C = {} ;
ex F being Function of NAT , bool X st
( rng F = {A,B,C} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = C ) ) by Th38;
hence {A,B,{} } is N_Sub_set_fam of X by A1, SUPINF_2:def 14; :: thesis: verum