set A = POSAltCat P;

thus POSAltCat P is transitive :: thesis: not POSAltCat P is empty

thus POSAltCat P is transitive :: thesis: not POSAltCat P is empty

proof

thus
not POSAltCat P is empty
by Def9; :: thesis: verum
let o1, o2, o3 be Object of (POSAltCat P); :: according to ALTCAT_1:def 2 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )

reconsider o19 = o1, o29 = o2, o39 = o3 as Element of P by Def9;

assume that

A1: <^o1,o2^> <> {} and

A2: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}

MonFuncs (o19,o29) <> {} by A1, Def9;

then consider f being object such that

A3: f in MonFuncs (o19,o29) by XBOOLE_0:def 1;

MonFuncs (o29,o39) <> {} by A2, Def9;

then consider g being object such that

A4: g in MonFuncs (o29,o39) by XBOOLE_0:def 1;

reconsider f = f, g = g as Function by A3, A4;

g * f in MonFuncs (o19,o39) by A3, A4, Th6;

hence not <^o1,o3^> = {} by Def9; :: thesis: verum

end;reconsider o19 = o1, o29 = o2, o39 = o3 as Element of P by Def9;

assume that

A1: <^o1,o2^> <> {} and

A2: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}

MonFuncs (o19,o29) <> {} by A1, Def9;

then consider f being object such that

A3: f in MonFuncs (o19,o29) by XBOOLE_0:def 1;

MonFuncs (o29,o39) <> {} by A2, Def9;

then consider g being object such that

A4: g in MonFuncs (o29,o39) by XBOOLE_0:def 1;

reconsider f = f, g = g as Function by A3, A4;

g * f in MonFuncs (o19,o39) by A3, A4, Th6;

hence not <^o1,o3^> = {} by Def9; :: thesis: verum