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 Def14;
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, Def16
.= (MSAlg_meet U0) . (x,y) by A1, MSUALG_2:def 21 ;
hence (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) ; :: thesis: verum