let T be non empty TopSpace; for a, b being Element of (Closed_Domains_Lattice T)
for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )
let a, b be Element of (Closed_Domains_Lattice T); for A, B being Element of Closed_Domains_of T st a = A & b = B holds
( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )
let A, B be Element of Closed_Domains_of T; ( a = A & b = B implies ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) ) )
assume that
A1:
a = A
and
A2:
b = B
; ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )
A3:
Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #)
by TDLAT_1:def 8;
hence a "\/" b =
(CLD-Union T) . (A,B)
by A1, A2, LATTICES:def 1
.=
A \/ B
by TDLAT_1:def 6
;
a "/\" b = Cl (Int (A /\ B))
thus a "/\" b =
(CLD-Meet T) . (A,B)
by A3, A1, A2, LATTICES:def 2
.=
Cl (Int (A /\ B))
by TDLAT_1:def 7
; verum