set f = ClMap T;
A1: (ClMap T) . ({} T) = Cl ({} T) by ROUGHS_2:def 15
.= {} T by PRE_TOPC:22 ;
(ClMap T) . ([#] T) = Cl ([#] T) by ROUGHS_2:def 15
.= [#] T by PRE_TOPC:22 ;
then A2: ( ClMap T is empty-preserving & ClMap T is universe-preserving ) by A1;
for A being Subset of T holds A c= (ClMap T) . A
proof
let A be Subset of T; :: thesis: A c= (ClMap T) . A
A c= Cl A by PRE_TOPC:18;
hence A c= (ClMap T) . A by ROUGHS_2:def 15; :: thesis: verum
end;
then A3: ClMap T is extensive ;
A4: ClMap T is idempotent
proof
for A being Subset of T holds (ClMap T) . A = (ClMap T) . ((ClMap T) . A)
proof
let A be Subset of T; :: thesis: (ClMap T) . A = (ClMap T) . ((ClMap T) . A)
(ClMap T) . A = Cl (Cl A) by ROUGHS_2:def 15
.= (ClMap T) . (Cl A) by ROUGHS_2:def 15
.= (ClMap T) . ((ClMap T) . A) by ROUGHS_2:def 15 ;
hence (ClMap T) . A = (ClMap T) . ((ClMap T) . A) ; :: thesis: verum
end;
hence ClMap T is idempotent ; :: thesis: verum
end;
for A, B being Subset of T holds (ClMap T) . (A \/ B) = ((ClMap T) . A) \/ ((ClMap T) . B)
proof
let A, B be Subset of T; :: thesis: (ClMap T) . (A \/ B) = ((ClMap T) . A) \/ ((ClMap T) . B)
(ClMap T) . (A \/ B) = Cl (A \/ B) by ROUGHS_2:def 15
.= (Cl A) \/ (Cl B) by PRE_TOPC:20
.= ((ClMap T) . A) \/ (Cl B) by ROUGHS_2:def 15
.= ((ClMap T) . A) \/ ((ClMap T) . B) by ROUGHS_2:def 15 ;
hence (ClMap T) . (A \/ B) = ((ClMap T) . A) \/ ((ClMap T) . B) ; :: thesis: verum
end;
then ClMap T is \/-preserving ;
hence ClMap T is closure by A2, A3, A4; :: thesis: verum