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