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 b1 being M3( the carrier of BB)
for b2 being M3( the carrier of (A opp)) holds
( not b1 = b2 or idm b2 in <^b1,b1^> )
let o be Object of BB; :: thesis: for b1 being M3( the carrier of (A opp)) holds
( not o = b1 or idm b1 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;
end;
end;
hence B opp is subcategory of A opp ; :: thesis: verum