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;
A4: G c= B by A2;
let x be object ; :: 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 reconsider xx = x as Element of B ;
A6: xx is_/\-irreducible_in B by A5, Def3;
assume A7: not x in G \/ {X} ; :: thesis: contradiction
then not x in {X} by XBOOLE_0:def 3;
then A8: x <> X by TARSKI:def 1;
x in B by A5;
then consider S being Subset-Family of X such that
A9: x = Intersect S and
A10: S c= G by A3;
not x in S by A10, A7, XBOOLE_0:def 3;
hence contradiction by A1, A4, A9, A10, A8, A6, Th4, XBOOLE_1:1; :: thesis: verum