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 )

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

hence
S = X \ S
by TARSKI:2; :: thesis: verum
let A be object ; :: thesis: ( A in S iff A in X \ 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;hereby :: thesis: ( A in X \ S implies A in S )

assume A2:
A in X \ S
; :: thesis: A in Sassume 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;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

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