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 set ; :: 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 8;
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;

let X1 be set ; :: 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 A2: X1 in { (Y ` ) where Y is Subset of X : Y in S } ; :: thesis: X1 in dual S
consider Y being Subset of X such that
A3: Y ` = X1 and
A4: Y in S by A2;
(Y ` ) ` in S by A4;
hence X1 in dual S by A3, SETFAM_1:def 8; :: thesis: verum