let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1
for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . x,y = (MSAlg_meet U0) . x,y
let U0 be non-empty OSAlgebra of S1; :: thesis: for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . x,y = (MSAlg_meet U0) . x,y
let x, y be Element of OSSub U0; :: thesis: (OSAlg_meet U0) . x,y = (MSAlg_meet U0) . x,y
( x is strict OSSubAlgebra of U0 & y is strict OSSubAlgebra of U0 ) by Def15;
then consider U1, U2 being strict OSSubAlgebra of U0 such that
A1: ( x = U1 & y = U2 ) ;
(OSAlg_meet U0) . x,y = U1 /\ U2 by A1, Def17
.= (MSAlg_meet U0) . x,y by A1, MSUALG_2:def 22 ;
hence (OSAlg_meet U0) . x,y = (MSAlg_meet U0) . x,y ; :: thesis: verum