let X, G be set ; :: thesis: for B being non empty finite Subset-Family of X st B is (B1) & B is (B2) & G is_generator-set_of B holds
/\-IRR B c= G \/ {X}
let B be non empty finite Subset-Family of X; :: thesis: ( B is (B1) & B is (B2) & G is_generator-set_of B implies /\-IRR B c= G \/ {X} )
assume that
A1: ( B is (B1) & B is (B2) ) and
A2: G is_generator-set_of B ; :: thesis: /\-IRR B c= G \/ {X}
A3: B = { (Intersect S) where S is Subset-Family of X : S c= G } by A2, Def26;
A4: G c= B by A2, Def26;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in /\-IRR B or x in G \/ {X} )
assume A5: x in /\-IRR B ; :: thesis: x in G \/ {X}
then x in B ;
then consider S being Subset-Family of X such that
A6: x = Intersect S and
A7: S c= G by A3;
assume A9: not x in G \/ {X} ; :: thesis: contradiction
then ( not x in G & not x in {X} ) by XBOOLE_0:def 3;
then A10: ( not x in G & x <> X ) by TARSKI:def 1;
A11: not x in S by A7, A9, XBOOLE_0:def 3;
reconsider xx = x as Element of B by A5;
xx is_/\-irreducible_in B by A5, Def3;
hence contradiction by A1, A4, A6, A7, A10, A11, Th4, XBOOLE_1:1; :: thesis: verum