let X be set ; :: thesis: for A, B, A9, B9 being Subset of X holds
( [A,B] >= [A9,B9] iff ( A c= A9 & B9 c= B ) )
let A, B, A9, B9 be Subset of X; :: thesis: ( [A,B] >= [A9,B9] iff ( A c= A9 & B9 c= B ) )
A1: [A,B] `2 = B by MCART_1:def 2;
A2: [A9,B9] `1 = A9 by MCART_1:def 1;
A3: [A9,B9] `2 = B9 by MCART_1:def 2;
[A,B] `1 = A by MCART_1:def 1;
hence ( [A,B] >= [A9,B9] iff ( A c= A9 & B9 c= B ) ) by A1, A2, A3, Def10; :: thesis: verum