set B = {X};
reconsider B = {X} as Subset-Family of X by ZFMISC_1:80;
take B ; :: thesis: ( B is (B1) & B is (B2) )
X in B by TARSKI:def 1;
hence B is (B1) by Def4; :: thesis: B is (B2)
thus B is (B2) :: thesis: verum

proof

let a, b be set ; :: according to FINSUB_1:def 2 :: thesis: ( not a in B or not b in B or a /\ b in B )
assume ( a in B & b in B ) ; :: thesis: a /\ b in B
then ( a = X & b = X ) by TARSKI:def 1;
hence a /\ b in B by TARSKI:def 1; :: thesis: verum

end;