hereby :: thesis: ( ( for A being set st A in IT holds

X \ A in IT ) implies IT is compl-closed )

assume A3:
for A being set st A in IT holds X \ A in IT ) implies IT is compl-closed )

assume A1:
IT is compl-closed
; :: thesis: for A being set st A in IT holds

X \ A in IT

let A be set ; :: thesis: ( A in IT implies X \ A in IT )

assume A2: A in IT ; :: thesis: X \ A in IT

then reconsider A9 = A as Subset of X ;

A9 ` in IT by A1, A2;

hence X \ A in IT ; :: thesis: verum

end;X \ A in IT

let A be set ; :: thesis: ( A in IT implies X \ A in IT )

assume A2: A in IT ; :: thesis: X \ A in IT

then reconsider A9 = A as Subset of X ;

A9 ` in IT by A1, A2;

hence X \ A in IT ; :: thesis: verum

X \ A in IT ; :: thesis: IT is compl-closed

let A be Subset of X; :: according to PROB_1:def 1 :: thesis: ( not A in IT or A ` in IT )

assume A in IT ; :: thesis: A ` in IT

hence A ` in IT by A3; :: thesis: verum