let A be category; :: thesis: for B being non empty subcategory of non empty holds B opp is subcategory of
let B be non empty subcategory of non empty ; :: thesis: B opp is subcategory of
reconsider BB = B opp as non empty transitive SubCatStr of A opp by Th48;
A1: A opp ,A are_opposite by YELLOW18:def 4;
A2: BB,B are_opposite by YELLOW18:def 4;
BB is id-inheriting

proof

per cases ( not BB is empty or BB is empty ) ;
:: according to ALTCAT_2:def 14

case not BB is empty ; :: thesis: for b₁ being M2(the carrier of BB)
for b₂ being M2(the carrier of (A opp )) holds
( not b₁ = b₂ or idm b₂ in <^b₁,b₁^> )

let o be object of ; :: thesis: for b₁ being M2(the carrier of (A opp )) holds
( not o = b₁ or idm b₁ in <^o,o^> )
let o' be object of ; :: thesis: ( not o = o' or idm o' in <^o,o^> )
reconsider a' = o' as object of by A1, YELLOW18:def 3;
reconsider a = o as object of by A2, YELLOW18:def 3;
assume o = o' ; :: thesis: idm o' in <^o,o^>
then idm a' in <^a,a^> by ALTCAT_2:def 14;
then idm o' in <^a,a^> by A1, YELLOW18:10;
hence idm o' in <^o,o^> by A2, YELLOW18:7; :: thesis: verum

end;

case BB is empty ; :: thesis: verum

thus verum ; :: thesis: verum

end;

end;

end;

hence B opp is subcategory of ; :: thesis: verum