set L = LattStr(# (MSSub U0),(),() #);
A1: for a, b, c being Element of LattStr(# (MSSub U0),(),() #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c by ;
A2: for a, b being Element of LattStr(# (MSSub U0),(),() #) holds a "/\" b = b "/\" a by ;
A3: for a, b being Element of LattStr(# (MSSub U0),(),() #) holds a "/\" (a "\/" b) = a
proof
let a, b be Element of LattStr(# (MSSub U0),(),() #); :: thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of MSSub U0 ;
(MSAlg_meet U0) . (x,(() . (x,y))) = x
proof
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
(MSAlg_join U0) . (x,y) = U1 "\/" U2 by Def20;
hence () . (x,(() . (x,y))) = U1 /\ (U1 "\/" U2) by Def21
.= x by Th27 ;
:: thesis: verum
end;
hence a "/\" (a "\/" b) = a ; :: thesis: verum
end;
A4: for a, b being Element of LattStr(# (MSSub U0),(),() #) holds (a "/\" b) "\/" b = b
proof
let a, b be Element of LattStr(# (MSSub U0),(),() #); :: thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of MSSub U0 ;
(MSAlg_join U0) . ((() . (x,y)),y) = y
proof
reconsider U1 = x, U2 = y as strict MSSubAlgebra of U0 by Def19;
(MSAlg_meet U0) . (x,y) = U1 /\ U2 by Def21;
hence () . ((() . (x,y)),y) = (U1 /\ U2) "\/" U2 by Def20
.= y by Th28 ;
:: thesis: verum
end;
hence (a "/\" b) "\/" b = b ; :: thesis: verum
end;
A5: for a, b, c being Element of LattStr(# (MSSub U0),(),() #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c by ;
for a, b being Element of LattStr(# (MSSub U0),(),() #) holds a "\/" b = b "\/" a by ;
then ( LattStr(# (MSSub U0),(),() #) is strict & LattStr(# (MSSub U0),(),() #) is join-commutative & LattStr(# (MSSub U0),(),() #) is join-associative & LattStr(# (MSSub U0),(),() #) is meet-absorbing & LattStr(# (MSSub U0),(),() #) is meet-commutative & LattStr(# (MSSub U0),(),() #) is meet-associative & LattStr(# (MSSub U0),(),() #) is join-absorbing ) by A1, A4, A2, A5, A3;
hence LattStr(# (MSSub U0),(),() #) is strict Lattice ; :: thesis: verum