set PTA = ParsedTermsOSA X;
let L1, L2 be monotone OSCongruence of ParsedTermsOSA X; :: thesis: ( ( for R being monotone OSCongruence of ParsedTermsOSA X holds L1 c= R ) & ( for R being monotone OSCongruence of ParsedTermsOSA X holds L2 c= R ) implies L1 = L2 )
assume that
A36: for R being monotone OSCongruence of ParsedTermsOSA X holds L1 c= R and
A37: for R being monotone OSCongruence of ParsedTermsOSA X holds L2 c= R ; :: thesis: L1 = L2
( L1 c= L2 & L2 c= L1 ) by A36, A37;
hence L1 = L2 by PBOOLE:def 13; :: thesis: verum