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