take f ; :: according to INDEX_1:def 4 :: thesis: ex g being ManySortedSet of B st [f,g] = [f,g]
take g ; :: thesis: [f,g] = [f,g]
thus [f,g] = [f,g] ; :: thesis: verum