let X be set ; :: thesis: for S being Field_Subset of X holds S = X \ S
let S be Field_Subset of X; :: thesis: S = X \ S
for A being object holds
( A in S iff A in X \ S )

proof

let A be object ; :: thesis: ( A in S iff A in X \ S )

hereby :: thesis: ( A in X \ S implies A in S )

assume A1: A in S ; :: thesis: A in X \ S
then reconsider B = A as Subset of X ;
B ` in S by A1, PROB_1:def 1;
hence A in X \ S by SETFAM_1:def 7; :: thesis: verum

end;

assume A2: A in X \ S ; :: thesis: A in S
then reconsider B = A as Subset of X ;
B ` in S by A2, SETFAM_1:def 7;
then (B `) ` in S by PROB_1:def 1;
hence A in S ; :: thesis: verum

end;

hence S = X \ S by TARSKI:2; :: thesis: verum