let T be non empty TopSpace; :: thesis: LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice
set L = LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #);

A1: now :: thesis: for p, q being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "\/" q = q "\/" p

let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); :: thesis: p "\/" q = q "\/" p
thus p "\/" q = q \/ p by Def2
.= q "\/" p by Def2 ; :: thesis: verum

end;

A2: now :: thesis: for p, q being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds (p "/\" q) "\/" q = q

let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); :: thesis: (p "/\" q) "\/" q = q
thus (p "/\" q) "\/" q = (p "/\" q) \/ q by Def2
.= (p /\ q) \/ q by Def3
.= q by XBOOLE_1:22 ; :: thesis: verum

end;

A3: now :: thesis: for p, q being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "/\" (p "\/" q) = p

let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); :: thesis: p "/\" (p "\/" q) = p
thus p "/\" (p "\/" q) = p /\ (p "\/" q) by Def3
.= p /\ (p \/ q) by Def2
.= p by XBOOLE_1:21 ; :: thesis: verum

end;

A4: now :: thesis: for p, q, r being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "/\" (q "/\" r) = (p "/\" q) "/\" r

let p, q, r be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); :: thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
thus p "/\" (q "/\" r) = p /\ (q "/\" r) by Def3
.= p /\ (q /\ r) by Def3
.= (p /\ q) /\ r by XBOOLE_1:16
.= (p "/\" q) /\ r by Def3
.= (p "/\" q) "/\" r by Def3 ; :: thesis: verum

end;

A5: now :: thesis: for p, q being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "/\" q = q "/\" p

let p, q be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); :: thesis: p "/\" q = q "/\" p
thus p "/\" q = q /\ p by Def3
.= q "/\" p by Def3 ; :: thesis: verum

end;

now :: thesis: for p, q, r being Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) holds p "\/" (q "\/" r) = (p "\/" q) "\/" r

let p, q, r be Element of LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #); :: thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
thus p "\/" (q "\/" r) = p \/ (q "\/" r) by Def2
.= p \/ (q \/ r) by Def2
.= (p \/ q) \/ r by XBOOLE_1:4
.= (p "\/" q) \/ r by Def2
.= (p "\/" q) "\/" r by Def2 ; :: thesis: verum

end;

then ( LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-commutative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-associative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-absorbing & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-commutative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is meet-associative & LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is join-absorbing ) by A1, A2, A5, A4, A3;
hence LattStr(# (Topology_of T),(Top_Union T),(Top_Meet T) #) is Lattice ; :: thesis: verum