set L = LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #);

A1: for a, b, c being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c by Th30, BINOP_1:def 3;

A2: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" b = b "/\" a by Th31, BINOP_1:def 2;

A3: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" (a "\/" b) = a

for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "\/" b = b "\/" a by Th29, BINOP_1:def 2;

then ( LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-commutative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-associative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-absorbing & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-commutative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-associative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-absorbing ) by A1, A4, A2, A5, A3;

hence LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice ; :: thesis: verum

A1: for a, b, c being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c by Th30, BINOP_1:def 3;

A2: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" b = b "/\" a by Th31, BINOP_1:def 2;

A3: for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" (a "\/" b) = a

proof

A4:
for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds (a "/\" b) "\/" b = b
let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); :: thesis: a "/\" (a "\/" b) = a

reconsider x = a, y = b as Element of MSSub U0 ;

(MSAlg_meet U0) . (x,((MSAlg_join U0) . (x,y))) = x

end;reconsider x = a, y = b as Element of MSSub U0 ;

(MSAlg_meet U0) . (x,((MSAlg_join U0) . (x,y))) = x

proof

hence
a "/\" (a "\/" b) = a
; :: thesis: verum
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;

(MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20;

hence (MSAlg_meet U0) . (x,((MSAlg_join U0) . (x,y))) = U1 /\ (U1 "\/" U2) by Def21

.= x by Th27 ;

:: thesis: verum

end;(MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20;

hence (MSAlg_meet U0) . (x,((MSAlg_join U0) . (x,y))) = U1 /\ (U1 "\/" U2) by Def21

.= x by Th27 ;

:: thesis: verum

proof

A5:
for a, b, c being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
by Th32, BINOP_1:def 3;
let a, b be Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #); :: thesis: (a "/\" b) "\/" b = b

reconsider x = a, y = b as Element of MSSub U0 ;

(MSAlg_join U0) . (((MSAlg_meet U0) . (x,y)),y) = y

end;reconsider x = a, y = b as Element of MSSub U0 ;

(MSAlg_join U0) . (((MSAlg_meet U0) . (x,y)),y) = y

proof

hence
(a "/\" b) "\/" b = b
; :: thesis: verum
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;

(MSAlg_meet U0) . (x,y) = U1 /\ U2 by Def21;

hence (MSAlg_join U0) . (((MSAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/" U2 by Def20

.= y by Th28 ;

:: thesis: verum

end;(MSAlg_meet U0) . (x,y) = U1 /\ U2 by Def21;

hence (MSAlg_join U0) . (((MSAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/" U2 by Def20

.= y by Th28 ;

:: thesis: verum

for a, b being Element of LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) holds a "\/" b = b "\/" a by Th29, BINOP_1:def 2;

then ( LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-commutative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-associative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-absorbing & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-commutative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is meet-associative & LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is join-absorbing ) by A1, A4, A2, A5, A3;

hence LattStr(# (MSSub U0),(MSAlg_join U0),(MSAlg_meet U0) #) is strict Lattice ; :: thesis: verum