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 Th47;
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 M3( the carrier of BB)
for b₂ being M3( 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 M3( the carrier of (A opp)) holds
( not o = b₁ or idm b₁ in <^o,o^> )
let o9 be Object of (A opp); :: thesis: ( not o = o9 or idm o9 in <^o,o^> )
reconsider a9 = o9 as Object of A by A1, YELLOW18:def 3;
reconsider a = o as Object of B by A2, YELLOW18:def 3;
assume o = o9 ; :: thesis: idm o9 in <^o,o^>
then idm a9 in <^a,a^> by ALTCAT_2:def 14;
then idm o9 in <^a,a^> by A1, YELLOW18:10;
hence idm o9 in <^o,o^> by A2, YELLOW18:7; :: thesis: verum

end;

case BB is empty ; :: thesis: verum

end;

end;

end;

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