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 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;