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