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 Th25;
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 Th26;
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 Def14;
(UniAlg_join U0) . (x,y) = U1 "\/" U2 by Def15;
hence (UniAlg_meet U0) . (x,((UniAlg_join U0) . (x,y))) = U1 /\ (U1 "\/" U2) by Def16
.= x by Th22 ;
:: 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 Def14;
(UniAlg_meet U0) . (x,y) = U1 /\ U2 by Def16;
hence (UniAlg_join U0) . (((UniAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/" U2 by Def15
.= y by Th23 ;
:: 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 Th27;
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 Th24;
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