let T be TopSpace; :: thesis: Flip (ClMap T) = IntMap T
set f = Flip (ClMap T);
set g = IntMap T;
for x being Subset of T holds (Flip (ClMap T)) . x = (IntMap T) . x
proof
let x be Subset of T; :: thesis: (Flip (ClMap T)) . x = (IntMap T) . x
A1: (Int x) ` = Cl (x `) by TDLAT_3:2;
(Flip (ClMap T)) . x = ((ClMap T) . (x `)) ` by Def14
.= (Cl (x `)) ` by Def15
.= (IntMap T) . x by Def16, A1 ;
hence (Flip (ClMap T)) . x = (IntMap T) . x ; :: thesis: verum
end;
hence Flip (ClMap T) = IntMap T ; :: thesis: verum