let N be Cardinal; :: thesis: for X being non empty set
for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N
let X be non empty set ; :: thesis: for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N
let S be non empty Subset-Family of X; :: thesis: ( S is_multiplicative_with N implies dual S is_additive_with N )
assume A1: S is_multiplicative_with N ; :: thesis: dual S is_additive_with N
deffunc H₁( Subset of X) -> Element of bool X = $1 ` ;
let S1 be non empty set ; :: according to CARD_FIL:def 4 :: thesis: ( S1 c= dual S & card S1 in N implies union S1 in dual S )
assume that
A2: S1 c= dual S and
A3: card S1 in N ; :: thesis: union S1 in dual S
reconsider S2 = S1 as non empty Subset-Family of X by A2, XBOOLE_1:1;
set S3 = dual S2;
A4: card { H<sub>1</sub>(Y) where Y is Subset of X : Y in S2 } c= card S2 from TREES_2:sch 2();
{ (Y `) where Y is Subset of X : Y in S2 } = dual S2 by Th9;
then A5: card (dual S2) in N by A3, A4, ORDINAL1:12;
A6: (union S2) ` = ([#] X) \ (union S2)
.= meet (dual S2) by SETFAM_1:33 ;
dual S2 c= S by A2, SETFAM_1:37;
then ((meet (dual S2)) `) ` in S by A1, A5;
hence union S1 in dual S by A6, SETFAM_1:def 7; :: thesis: verum