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

proof

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;

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 )
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