let T be non empty TopSpace; :: thesis: LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice
set L = LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #);
A1: for p, q being Element of holds p "\/" q = q "\/" p

proof

let p, q be Element of ; :: thesis: p "\/" q = q "\/" p
consider p', q' being Element of OpenClosedSet T such that
A2: p = p' and
A3: q = q' ;
thus p "\/" q = q' \/ p' by A2, A3, Def2
.= q "\/" p by A2, A3, Def2 ; :: thesis: verum

end;

A4: for p, q, r being Element of holds p "\/" (q "\/" r) = (p "\/" q) "\/" r

proof

let p, q, r be Element of ; :: thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
consider p', q', r', k', l' being Element of OpenClosedSet T such that
A5: p = p' and
A6: q = q' and
A7: r = r' and
A8: q "\/" r = k' and
A9: p "\/" q = l' ;
thus p "\/" (q "\/" r) = p' \/ k' by A5, A8, Def2
.= p' \/ (q' \/ r') by A6, A7, A8, Def2
.= (p' \/ q') \/ r' by XBOOLE_1:4
.= l' \/ r' by A5, A6, A9, Def2
.= (p "\/" q) "\/" r by A7, A9, Def2 ; :: thesis: verum

end;

A10: for p, q being Element of holds (p "/\" q) "\/" q = q

proof

let p, q be Element of ; :: thesis: (p "/\" q) "\/" q = q
consider p', q', k' being Element of OpenClosedSet T such that
A11: p = p' and
A12: q = q' and
A13: p "/\" q = k' ;
thus (p "/\" q) "\/" q = k' \/ q' by A12, A13, Def2
.= (p' /\ q') \/ q' by A11, A12, A13, Def3
.= q by A12, XBOOLE_1:22 ; :: thesis: verum

end;

A14: for p, q being Element of holds p "/\" q = q "/\" p

proof

let p, q be Element of ; :: thesis: p "/\" q = q "/\" p
consider p', q' being Element of OpenClosedSet T such that
A15: p = p' and
A16: q = q' ;
thus p "/\" q = q' /\ p' by A15, A16, Def3
.= q "/\" p by A15, A16, Def3 ; :: thesis: verum

end;

A17: for p, q, r being Element of holds p "/\" (q "/\" r) = (p "/\" q) "/\" r

proof

let p, q, r be Element of ; :: thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
consider p', q', r', k', l' being Element of OpenClosedSet T such that
A18: p = p' and
A19: q = q' and
A20: r = r' and
A21: q "/\" r = k' and
A22: p "/\" q = l' ;
thus p "/\" (q "/\" r) = p' /\ k' by A18, A21, Def3
.= p' /\ (q' /\ r') by A19, A20, A21, Def3
.= (p' /\ q') /\ r' by XBOOLE_1:16
.= l' /\ r' by A18, A19, A22, Def3
.= (p "/\" q) "/\" r by A20, A22, Def3 ; :: thesis: verum

end;

for p, q being Element of holds p "/\" (p "\/" q) = p

proof

let p, q be Element of ; :: thesis: p "/\" (p "\/" q) = p
consider p', q', k' being Element of OpenClosedSet T such that
A23: p = p' and
A24: q = q' and
A25: p "\/" q = k' ;
thus p "/\" (p "\/" q) = p' /\ k' by A23, A25, Def3
.= p' /\ (p' \/ q') by A23, A24, A25, Def2
.= p by A23, XBOOLE_1:21 ; :: thesis: verum

end;

then ( LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is join-commutative & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is join-associative & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is meet-absorbing & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is meet-commutative & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is meet-associative & LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is join-absorbing ) by A1, A4, A10, A14, A17, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice ; :: thesis: verum