set L = LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #);
A1: for a, b, c being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c

proof

let a, b, c be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); :: thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
OSAlg_join U0 is associative by Th50;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c by BINOP_1:def 3; :: thesis: verum

end;

A2: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" b = b "/\" a

proof

let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); :: thesis: a "/\" b = b "/\" a
OSAlg_meet U0 is commutative by Th51;
hence a "/\" b = b "/\" a by BINOP_1:def 2; :: thesis: verum

end;

A3: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" (a "\/" b) = a

proof

let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); :: thesis: a "/\" (a "\/" b) = a
reconsider x = a, y = b as Element of OSSub U0 ;
(OSAlg_meet U0) . x,((OSAlg_join U0) . x,y) = x

proof

reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def15;
(OSAlg_join U0) . x,y = U1 "\/"_os U2 by Def16;
hence (OSAlg_meet U0) . x,((OSAlg_join U0) . x,y) = U1 /\ (U1 "\/"_os U2) by Def17
.= x by Th45 ;
:: thesis: verum

end;

hence a "/\" (a "\/" b) = a ; :: thesis: verum

end;

A4: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds (a "/\" b) "\/" b = b

proof

let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); :: thesis: (a "/\" b) "\/" b = b
reconsider x = a, y = b as Element of OSSub U0 ;
(OSAlg_join U0) . ((OSAlg_meet U0) . x,y),y = y

proof

reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def15;
(OSAlg_meet U0) . x,y = U1 /\ U2 by Def17;
hence (OSAlg_join U0) . ((OSAlg_meet U0) . x,y),y = (U1 /\ U2) "\/"_os U2 by Def16
.= y by Th46 ;
:: thesis: verum

end;

hence (a "/\" b) "\/" b = b ; :: thesis: verum

end;

A5: for a, b, c being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c

proof

let a, b, c be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); :: thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
OSAlg_meet U0 is associative by Th52;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c by BINOP_1:def 3; :: thesis: verum

end;

for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "\/" b = b "\/" a

proof

let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); :: thesis: a "\/" b = b "\/" a
OSAlg_join U0 is commutative by Th49;
hence a "\/" b = b "\/" a by BINOP_1:def 2; :: thesis: verum

end;

then ( LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-commutative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-associative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-absorbing & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-commutative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-associative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-absorbing ) by A1, A4, A2, A5, A3, LATTICES:def 4, LATTICES:def 5, LATTICES:def 6, LATTICES:def 7, LATTICES:def 8, LATTICES:def 9;
hence LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict Lattice ; :: thesis: verum