let T be non empty TopSpace; :: thesis: 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); :: thesis: 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; :: thesis: ( a = A & b = B implies ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) ) )
A1: Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) by TDLAT_1:def 8;
assume A2: ( a = A & b = B ) ; :: thesis: ( a "\/" b = A \/ B & a "/\" b = Cl (Int (A /\ B)) )
hence a "\/" b = (CLD-Union T) . A,B by A1, LATTICES:def 1
.= A \/ B by TDLAT_1:def 6 ;
:: thesis: a "/\" b = Cl (Int (A /\ B))
thus a "/\" b = (CLD-Meet T) . A,B by A1, A2, LATTICES:def 2
.= Cl (Int (A /\ B)) by TDLAT_1:def 7 ; :: thesis: verum