let A be category; :: thesis: for B being non empty subcategory of A holds B opp is subcategory of A opp
let B be non empty subcategory of A; :: thesis: B opp is subcategory of A opp
reconsider BB = B opp as non empty transitive SubCatStr of A opp by Th48;
A1: ( BB,B are_opposite & A opp ,A 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 Element of the carrier of BB
for b₂ being Element of the carrier of (A opp ) holds
( not b₁ = b₂ or idm b₂ in <^b₁,b₁^> )

let o be object of BB; :: thesis: for b₁ being Element of the carrier of (A opp ) holds
( not o = b₁ or idm b₁ in <^o,o^> )
let o' be object of (A opp ); :: thesis: ( not o = o' or idm o' in <^o,o^> )
reconsider a = o as object of B by A1, YELLOW18:def 3;
reconsider a' = o' as object of A by A1, 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 A1, YELLOW18:7; :: thesis: verum

end;

case BB is empty ; :: thesis: verum

thus verum ; :: thesis: verum

end;

end;

end;

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