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,({} X)} & F . 0 = A & F . 1 = B & ( for n being Element of NAT st 1 < n holds
F . n = {} X ) ) by Th17;
hence {A,B,{}} is N_Sub_set_fam of X by SUPINF_2:def 8; :: thesis: verum