set A = POSAltCat P;
thus POSAltCat P is transitive :: thesis: not POSAltCat P is empty

proof

let o1, o2, o3 be object of ; :: according to ALTCAT_1:def 4 :: thesis: ( <^o1,o2^> = {} or <^o2,o3^> = {} or not <^o1,o3^> = {} )
reconsider o1' = o1, o2' = o2, o3' = o3 as Element of P by Def9;
assume that
A1: <^o1,o2^> <> {} and
A2: <^o2,o3^> <> {} ; :: thesis: not <^o1,o3^> = {}
MonFuncs o1',o2' <> {} by A1, Def9;
then consider f being set such that
A3: f in MonFuncs o1',o2' by XBOOLE_0:def 1;
MonFuncs o2',o3' <> {} by A2, Def9;
then consider g being set such that
A4: g in MonFuncs o2',o3' by XBOOLE_0:def 1;
reconsider f = f, g = g as Function by A3, A4;
g * f in MonFuncs o1',o3' by A3, A4, Th6;
hence not <^o1,o3^> = {} by Def9; :: thesis: verum

end;

thus not POSAltCat P is empty by Def9; :: thesis: verum