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 LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "\/" q = q "\/" p
proof
let p, q be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); :: thesis: p "\/" q = q "\/" p
consider p9, q9 being Element of OpenClosedSet T such that
A2: p = p9 and
A3: q = q9 ;
thus p "\/" q = q9 \/ p9 by A2, A3, Def2
.= q "\/" p by A2, A3, Def2 ; :: thesis: verum
end;
A4: for p, q, r being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "\/" (q "\/" r) = (p "\/" q) "\/" r
proof
let p, q, r be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); :: thesis: p "\/" (q "\/" r) = (p "\/" q) "\/" r
consider p9, q9, r9, k9, l9 being Element of OpenClosedSet T such that
A5: p = p9 and
A6: q = q9 and
A7: r = r9 and
A8: q "\/" r = k9 and
A9: p "\/" q = l9 ;
thus p "\/" (q "\/" r) = p9 \/ k9 by A5, A8, Def2
.= p9 \/ (q9 \/ r9) by A6, A7, A8, Def2
.= (p9 \/ q9) \/ r9 by XBOOLE_1:4
.= l9 \/ r9 by A5, A6, A9, Def2
.= (p "\/" q) "\/" r by A7, A9, Def2 ; :: thesis: verum
end;
A10: for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds (p "/\" q) "\/" q = q
proof
let p, q be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); :: thesis: (p "/\" q) "\/" q = q
consider p9, q9, k9 being Element of OpenClosedSet T such that
A11: p = p9 and
A12: q = q9 and
A13: p "/\" q = k9 ;
thus (p "/\" q) "\/" q = k9 \/ q9 by A12, A13, Def2
.= (p9 /\ q9) \/ q9 by A11, A12, A13, Def3
.= q by A12, XBOOLE_1:22 ; :: thesis: verum
end;
A14: for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" q = q "/\" p
proof
let p, q be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); :: thesis: p "/\" q = q "/\" p
consider p9, q9 being Element of OpenClosedSet T such that
A15: p = p9 and
A16: q = q9 ;
thus p "/\" q = q9 /\ p9 by A15, A16, Def3
.= q "/\" p by A15, A16, Def3 ; :: thesis: verum
end;
A17: for p, q, r being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" (q "/\" r) = (p "/\" q) "/\" r
proof
let p, q, r be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); :: thesis: p "/\" (q "/\" r) = (p "/\" q) "/\" r
consider p9, q9, r9, k9, l9 being Element of OpenClosedSet T such that
A18: p = p9 and
A19: q = q9 and
A20: r = r9 and
A21: q "/\" r = k9 and
A22: p "/\" q = l9 ;
thus p "/\" (q "/\" r) = p9 /\ k9 by A18, A21, Def3
.= p9 /\ (q9 /\ r9) by A19, A20, A21, Def3
.= (p9 /\ q9) /\ r9 by XBOOLE_1:16
.= l9 /\ r9 by A18, A19, A22, Def3
.= (p "/\" q) "/\" r by A20, A22, Def3 ; :: thesis: verum
end;
for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" (p "\/" q) = p
proof
let p, q be Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #); :: thesis: p "/\" (p "\/" q) = p
consider p9, q9, k9 being Element of OpenClosedSet T such that
A23: p = p9 and
A24: q = q9 and
A25: p "\/" q = k9 ;
thus p "/\" (p "\/" q) = p9 /\ k9 by A23, A25, Def3
.= p9 /\ (p9 \/ q9) 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;
hence LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice ; :: thesis: verum