set B = {X};
reconsider B = {X} as Subset-Family of X by ZFMISC_1:68;
take B ; :: thesis: ( B is (B1) & B is (B2) )
X in B by TARSKI:def 1;
hence B is (B1) ; :: 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 that
A1: a in B and
A2: b in B ; :: thesis: a /\ b in B
A3: b = X by A2, TARSKI:def 1;
a = X by A1, TARSKI:def 1;
hence a /\ b in B by A3, TARSKI:def 1; :: thesis: verum
end;