hereby :: thesis: ( ( 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;
assume A3: for A being set st A in IT holds
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