let C be initialized ConstructorSignature; :: thesis: for f being valuation of C
for A, B being Subset of (QuasiAdjs C) st A c= B holds
A at f c= B at f
let f be valuation of C; :: thesis: for A, B being Subset of (QuasiAdjs C) st A c= B holds
A at f c= B at f
let A, B be Subset of (QuasiAdjs C); :: thesis: ( A c= B implies A at f c= B at f )
assume A c= B ; :: thesis: A at f c= B at f
then A \/ B = B by XBOOLE_1:12;
then B at f = (A at f) \/ (B at f) by Th145;
hence A at f c= B at f by XBOOLE_1:7; :: thesis: verum