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_{1}( 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_{1}(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

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

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

{ (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