let Y be set ; :: thesis: ( Y is subset-closed iff for X being set st X in Y holds
bool X c= Y )
thus ( Y is subset-closed implies for X being set st X in Y holds
bool X c= Y ) ; :: thesis: ( ( for X being set st X in Y holds
bool X c= Y ) implies Y is subset-closed )
assume A1: 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
A2: x in Y and
A3: y c= x ; :: thesis: y in Y
A4: y in bool x by A3;
bool x c= Y by A1, A2;
hence y in Y by A4; :: thesis: verum