let X be set ; :: thesis: for K being Subset of X
for B being Subset-Family of X st B = {X} \/ { A where A is Subset of X : not K c= A } holds
( B is (B1) & B is (B2) )
let K be Subset of X; :: thesis: for B being Subset-Family of X st B = {X} \/ { A where A is Subset of X : not K c= A } holds
( B is (B1) & B is (B2) )
let BB be Subset-Family of X; :: thesis: ( BB = {X} \/ { A where A is Subset of X : not K c= A } implies ( BB is (B1) & BB is (B2) ) )
assume A1: BB = {X} \/ { B where B is Subset of X : not K c= B } ; :: thesis: ( BB is (B1) & BB is (B2) )
X in {X} by TARSKI:def 1;
then X in BB by A1, XBOOLE_0:def 3;
hence BB is (B1) ; :: thesis: BB is (B2)
set BB1 = { B where B is Subset of X : not K c= B } ;
thus BB is (B2) :: thesis: verum

proof

let a, b be set ; :: according to FINSUB_1:def 2 :: thesis: ( not a in BB or not b in BB or a /\ b in BB )
assume that
A2: a in BB and
A3: b in BB ; :: thesis: a /\ b in BB
reconsider a9 = a, b9 = b as Subset of X by A2, A3;

per cases ( ( a in {X} & b in {X} ) or ( a in {X} & b in { B where B is Subset of X : not K c= B } ) or ( a in { B where B is Subset of X : not K c= B } & b in {X} ) or ( a in { B where B is Subset of X : not K c= B } & b in { B where B is Subset of X : not K c= B } ) ) by A1, A2, A3, XBOOLE_0:def 3;

suppose A4: ( a in {X} & b in {X} ) ; :: thesis: a /\ b in BB

then A5: b = X by TARSKI:def 1;
a = X by A4, TARSKI:def 1;
then a /\ b in {X} by A5, TARSKI:def 1;
hence a /\ b in BB by A1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A6: ( a in {X} & b in { B where B is Subset of X : not K c= B } ) ; :: thesis: a /\ b in BB

then a = X by TARSKI:def 1;
then a9 /\ b9 = b by XBOOLE_1:28;
hence a /\ b in BB by A1, A6, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A7: ( a in { B where B is Subset of X : not K c= B } & b in {X} ) ; :: thesis: a /\ b in BB

then b = X by TARSKI:def 1;
then a9 /\ b9 = a by XBOOLE_1:28;
hence a /\ b in BB by A1, A7, XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( a in { B where B is Subset of X : not K c= B } & b in { B where B is Subset of X : not K c= B } ) ; :: thesis: a /\ b in BB

then ex B1 being Subset of X st
( b = B1 & not K c= B1 ) ;
then not K c= a /\ b by XBOOLE_1:18;
then a9 /\ b9 in { B where B is Subset of X : not K c= B } ;
hence a /\ b in BB by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;