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
{} is Subset of X by XBOOLE_1:2;
then consider C being Subset of X 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