let Y be set ; :: thesis: ( Y is subset-closed iff for X being set st X in Y holds
bool X c= Y )

hereby :: thesis: ( ( for X being set st X in Y holds
bool X c= Y ) implies Y is subset-closed )

assume A1: Y is subset-closed ; :: thesis: for X being set st X in Y holds
bool X c= Y
let X be set ; :: thesis: ( X in Y implies bool X c= Y )
assume A2: X in Y ; :: thesis: bool X c= Y
thus bool X c= Y :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool X or x in Y )
assume x in bool X ; :: thesis: x in Y
hence x in Y by A1, A2, CLASSES1:def 1; :: thesis: verum

end;

end;

assume A3: for X being set st X in Y holds
bool X c= Y ; :: thesis: Y is subset-closed
let x be set ; :: according to CLASSES1:def 1 :: thesis: for b₁ being set holds
( not x in Y or not b₁ c= x or b₁ in Y )
let y be set ; :: thesis: ( not x in Y or not y c= x or y in Y )
assume that
A4: x in Y and
A5: y c= x ; :: thesis: y in Y
A6: y in bool x by A5;
bool x c= Y by A3, A4;
hence y in Y by A6; :: thesis: verum