let X be non empty set ; :: thesis: for S being non empty Subset-Family of X holds dual S = { (Y `) where Y is Subset of X : Y in S }

let S be non empty Subset-Family of X; :: thesis: dual S = { (Y `) where Y is Subset of X : Y in S }

thus dual S c= { (Y `) where Y is Subset of X : Y in S } :: according to XBOOLE_0:def 10 :: thesis: { (Y `) where Y is Subset of X : Y in S } c= dual S

assume X1 in { (Y `) where Y is Subset of X : Y in S } ; :: thesis: X1 in dual S

then consider Y being Subset of X such that

A2: Y ` = X1 and

A3: Y in S ;

(Y `) ` in S by A3;

hence X1 in dual S by A2, SETFAM_1:def 7; :: thesis: verum

let S be non empty Subset-Family of X; :: thesis: dual S = { (Y `) where Y is Subset of X : Y in S }

thus dual S c= { (Y `) where Y is Subset of X : Y in S } :: according to XBOOLE_0:def 10 :: thesis: { (Y `) where Y is Subset of X : Y in S } c= dual S

proof

let X1 be object ; :: according to TARSKI:def 3 :: thesis: ( not X1 in { (Y `) where Y is Subset of X : Y in S } or X1 in dual S )
let X1 be object ; :: according to TARSKI:def 3 :: thesis: ( not X1 in dual S or X1 in { (Y `) where Y is Subset of X : Y in S } )

assume A1: X1 in dual S ; :: thesis: X1 in { (Y `) where Y is Subset of X : Y in S }

reconsider Y1 = X1 as Subset of X by A1;

Y1 ` in S by A1, SETFAM_1:def 7;

then (Y1 `) ` in { (Y `) where Y is Subset of X : Y in S } ;

hence X1 in { (Y `) where Y is Subset of X : Y in S } ; :: thesis: verum

end;assume A1: X1 in dual S ; :: thesis: X1 in { (Y `) where Y is Subset of X : Y in S }

reconsider Y1 = X1 as Subset of X by A1;

Y1 ` in S by A1, SETFAM_1:def 7;

then (Y1 `) ` in { (Y `) where Y is Subset of X : Y in S } ;

hence X1 in { (Y `) where Y is Subset of X : Y in S } ; :: thesis: verum

assume X1 in { (Y `) where Y is Subset of X : Y in S } ; :: thesis: X1 in dual S

then consider Y being Subset of X such that

A2: Y ` = X1 and

A3: Y in S ;

(Y `) ` in S by A3;

hence X1 in dual S by A2, SETFAM_1:def 7; :: thesis: verum