let X, Y be set ; :: thesis: ( X is_finer_than Y iff subset-closed_closure_of X c= subset-closed_closure_of Y )
set fx = subset-closed_closure_of X;
set fy = subset-closed_closure_of Y;

hereby :: thesis: ( subset-closed_closure_of X c= subset-closed_closure_of Y implies X is_finer_than Y )

assume A1: X is_finer_than Y ; :: thesis: subset-closed_closure_of X c= subset-closed_closure_of Y
thus subset-closed_closure_of X c= subset-closed_closure_of Y :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in subset-closed_closure_of X or x in subset-closed_closure_of Y )
reconsider xx = x as set by TARSKI:1;
assume x in subset-closed_closure_of X ; :: thesis: x in subset-closed_closure_of Y
then consider y being set such that
A2: xx c= y and
A3: y in X by Th2;
consider c being set such that
A4: c in Y and
A5: y c= c by A1, A3;
xx c= c by A2, A5;
hence x in subset-closed_closure_of Y by A4, Th2; :: thesis: verum

end;

end;

assume A6: subset-closed_closure_of X c= subset-closed_closure_of Y ; :: thesis: X is_finer_than Y
let x be set ; :: according to SETFAM_1:def 2 :: thesis: ( not x in X or ex b₁ being set st
( b₁ in Y & x c= b₁ ) )
assume x in X ; :: thesis: ex b₁ being set st
( b₁ in Y & x c= b₁ )
then x in subset-closed_closure_of X by Th2;
then ex y being set st
( x c= y & y in Y ) by A6, Th2;
hence ex b₁ being set st
( b₁ in Y & x c= b₁ ) ; :: thesis: verum