let X be set ; :: thesis: for B being non empty finite Subset-Family of X st B is (B1) & B is (B2) holds
/\-IRR B is_generator-set_of B
let B be non empty finite Subset-Family of X; :: thesis: ( B is (B1) & B is (B2) implies /\-IRR B is_generator-set_of B )
assume A1: ( B is (B1) & B is (B2) ) ; :: thesis: /\-IRR B is_generator-set_of B
set G = /\-IRR B;
set H = { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } ;
thus /\-IRR B c= B ; :: according to ARMSTRNG:def 25 :: thesis: B = { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B }
now :: thesis: for x being object holds
( ( x in B implies x in { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } ) & ( x in { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } implies x in B ) )
let x be object ; :: thesis: ( ( x in B implies x in { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } ) & ( x in { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } implies x in B ) )
hereby :: thesis: ( x in { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } implies x in B )
assume x in B ; :: thesis: x in { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B }
then reconsider xx = x as Element of B ;
consider yz being non empty Subset of B such that
A2: xx = meet yz and
A3: for s being set st s in yz holds
s is_/\-irreducible_in B by Th3;
reconsider yz = yz as non empty Subset-Family of X by XBOOLE_1:1;
A4: yz c= /\-IRR B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in yz or x in /\-IRR B )
reconsider xx = x as set by TARSKI:1;
assume x in yz ; :: thesis: x in /\-IRR B
then xx is_/\-irreducible_in B by A3;
hence x in /\-IRR B by Def3; :: thesis: verum
end;
Intersect yz = meet yz by SETFAM_1:def 9;
hence x in { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } by A2, A4; :: thesis: verum
end;
assume x in { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } ; :: thesis: x in B
then ex S being Subset-Family of X st
( x = Intersect S & S c= /\-IRR B ) ;
hence x in B by A1, Th1, XBOOLE_1:1; :: thesis: verum
end;
hence B = { (Intersect S) where S is Subset-Family of X : S c= /\-IRR B } by TARSKI:2; :: thesis: verum