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

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
hence
B opp is subcategory of A opp
; :: thesis: verum

per cases
( not BB is empty or BB is empty )
;

:: according to ALTCAT_2:def 14

end;:: according to ALTCAT_2:def 14

case
not BB is empty
; :: thesis: for b_{1} being M3( the carrier of BB)

for b_{2} being M3( the carrier of (A opp)) holds

( not b_{1} = b_{2} or idm b_{2} in <^b_{1},b_{1}^> )

end;for b

( not b

let o be Object of BB; :: thesis: for b_{1} being M3( the carrier of (A opp)) holds

( not o = b_{1} or idm b_{1} 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;( not o = b

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