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 ;
A2: [A9,B9] `1 = A9 ;
A3: [A9,B9] `2 = B9 ;
[A,B] `1 = A ;
hence ( [A,B] >= [A9,B9] iff ( A c= A9 & B9 c= B ) ) by A1, A2, A3, Def9; :: thesis: verum