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
A47: for R being monotone OSCongruence of ParsedTermsOSA X holds L1 c= R and
A48: for R being monotone OSCongruence of ParsedTermsOSA X holds L2 c= R ; :: thesis: L1 = L2
A49: L2 c= L1 by A48;
L1 c= L2 by A47;
hence L1 = L2 by A49, PBOOLE:146; :: thesis: verum