let T be non empty TopSpace; :: thesis: for a, b being Element of (Open_Domains_Lattice T)
for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )
let a, b be Element of (Open_Domains_Lattice T); :: thesis: for A, B being Element of Open_Domains_of T st a = A & b = B holds
( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )
let A, B be Element of Open_Domains_of T; :: thesis: ( a = A & b = B implies ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B ) )
A1: Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) by TDLAT_1:def 12;
assume A2: ( a = A & b = B ) ; :: thesis: ( a "\/" b = Int (Cl (A \/ B)) & a "/\" b = A /\ B )
hence a "\/" b = (OPD-Union T) . A,B by A1, LATTICES:def 1
.= Int (Cl (A \/ B)) by TDLAT_1:def 10 ;
:: thesis: a "/\" b = A /\ B
thus a "/\" b = (OPD-Meet T) . A,B by A1, A2, LATTICES:def 2
.= A /\ B by TDLAT_1:def 11 ; :: thesis: verum