let X be non empty set ; :: thesis: for R, S, T being Membership_Func of X st S c= & T c= holds
T c=
let R, S, T be Membership_Func of X; :: thesis: ( S c= & T c= implies T c= )
assume A1: ( S c= & T c= ) ; :: thesis: T c=
for x being Element of X holds R . x <= T . x

proof

let x be Element of X; :: thesis: R . x <= T . x
( R . x <= S . x & S . x <= T . x ) by A1;
hence R . x <= T . x by XXREAL_0:2; :: thesis: verum

end;

hence T c= ; :: thesis: verum