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 ex Y being Subset of X st

( Y = X1 & Y ` in S ) ;

hence X1 in dual S by 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;

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;

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 ex Y being Subset of X st

( Y = X1 & Y ` in S ) ;

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