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