set A = POSAltCat P;
thus
POSAltCat P is transitive
not POSAltCat P is empty proof
let o1,
o2,
o3 be
Object of
(POSAltCat P);
ALTCAT_1:def 2 ( <^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^> <> {}
;
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;
verum
end;
thus
not POSAltCat P is empty
by Def9; verum