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

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