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