set L = LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #);
A1: for a, b, c being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof

let a, b, c be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider x = a, y = b, z = c as Element of Sub U0 ;
A2: UniAlg_join U0 is associative by Th28;
thus a "\/" (b "\/" c) = the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . a,(b "\/" c) by LATTICES:def 1
.= (UniAlg_join U0) . x,((UniAlg_join U0) . y,z) by LATTICES:def 1
.= the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . a,b),c by A2, BINOP_1:def 3
.= (the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . a,b) "\/" c by LATTICES:def 1
.= (a "\/" b) "\/" c by LATTICES:def 1 ; :: thesis: verum

end;

A3: for a, b being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "/\" b = b "/\" a

proof

let a, b be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); :: thesis: a "/\" b = b "/\" a
reconsider x = a, y = b as Element of Sub U0 ;
A4: UniAlg_meet U0 is commutative by Th29;
thus a "/\" b = (UniAlg_meet U0) . x,y by LATTICES:def 2
.= the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . b,a by A4, BINOP_1:def 2
.= b "/\" a by LATTICES:def 2 ; :: thesis: verum

end;

A5: for a, b being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "/\" (a "\/" b) = a

proof

let a, b be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); :: thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of Sub U0 ;
A6: (UniAlg_meet U0) . x,((UniAlg_join U0) . x,y) = x

proof

reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def15;
(UniAlg_join U0) . x,y = U1 "\/" U2 by Def16;
hence (UniAlg_meet U0) . x,((UniAlg_join U0) . x,y) = U1 /\ (U1 "\/" U2) by Def17
.= x by Th25 ;
:: thesis: verum

end;

thus a "/\" (a "\/" b) = the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . a,(a "\/" b) by LATTICES:def 2
.= a by A6, LATTICES:def 1 ; :: thesis: verum

end;

A7: for a, b being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds (a "/\" b) "\/" b = b

proof

let a, b be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); :: thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of Sub U0 ;
A8: (UniAlg_join U0) . ((UniAlg_meet U0) . x,y),y = y

proof

reconsider U1 = x, U2 = y as strict SubAlgebra of U0 by Def15;
(UniAlg_meet U0) . x,y = U1 /\ U2 by Def17;
hence (UniAlg_join U0) . ((UniAlg_meet U0) . x,y),y = (U1 /\ U2) "\/" U2 by Def16
.= y by Th26 ;
:: thesis: verum

end;

thus (a "/\" b) "\/" b = the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (a "/\" b),b by LATTICES:def 1
.= b by A8, LATTICES:def 2 ; :: thesis: verum

end;

A9: for a, b, c being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof

let a, b, c be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider x = a, y = b, z = c as Element of Sub U0 ;
A10: UniAlg_meet U0 is associative by Th30;
thus a "/\" (b "/\" c) = the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . a,(b "/\" c) by LATTICES:def 2
.= (UniAlg_meet U0) . x,((UniAlg_meet U0) . y,z) by LATTICES:def 2
.= the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . (the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . a,b),c by A10, BINOP_1:def 3
.= (the L_meet of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . a,b) "/\" c by LATTICES:def 2
.= (a "/\" b) "/\" c by LATTICES:def 2 ; :: thesis: verum

end;

for a, b being Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) holds a "\/" b = b "\/" a

proof

let a, b be Element of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #); :: thesis: a "\/" b = b "\/" a
reconsider x = a, y = b as Element of Sub U0 ;
A11: UniAlg_join U0 is commutative by Th27;
thus a "\/" b = (UniAlg_join U0) . x,y by LATTICES:def 1
.= the L_join of LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) . b,a by A11, BINOP_1:def 2
.= b "\/" a by LATTICES:def 1 ; :: thesis: verum

end;

then ( LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is join-commutative & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is join-associative & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is meet-absorbing & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is meet-commutative & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is meet-associative & LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is join-absorbing ) by A1, A7, A3, A9, A5, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence LattStr(# (Sub U0),(UniAlg_join U0),(UniAlg_meet U0) #) is strict Lattice ; :: thesis: verum