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

hence LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice ; :: thesis: verum

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

A4:
for p, q, r being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "\/" (q "\/" r) = (p "\/" q) "\/" r
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;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

proof

A10:
for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds (p "/\" q) "\/" q = q
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;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

proof

A14:
for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" q = q "/\" p
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;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

proof

A17:
for p, q, r being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" (q "/\" r) = (p "/\" q) "/\" r
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;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

proof

for p, q being Element of LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) holds p "/\" (p "\/" q) = p
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;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

proof

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;
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;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

hence LattStr(# (OpenClosedSet T),(T_join T),(T_meet T) #) is Lattice ; :: thesis: verum