let a, b, c be object of (W -SUP_category); ( S1[a] & S1[b] & S1[c] & <^a,b^> <> {} & <^b,c^> <> {} implies for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f] )
assume that
A4:
<^a,b^> <> {}
and
A5:
<^b,c^> <> {}
; for f being Morphism of a,b
for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
let f be Morphism of a,b; for g being Morphism of b,c st S2[a,b,f] & S2[b,c,g] holds
S2[a,c,g * f]
let g be Morphism of b,c; ( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
A6:
<^a,c^> <> {}
by A4, A5, ALTCAT_1:def 4;
A7:
@ f = f
by A4, YELLOW21:def 7;
A8:
@ g = g
by A5, YELLOW21:def 7;
A9:
@ (g * f) = g * f
by A6, YELLOW21:def 7;
A10:
@ g is sups-preserving Function of (latt b),(latt c)
by A1, A5, A8, Def5;
A11:
@ f is sups-preserving Function of (latt a),(latt b)
by A1, A4, A7, Def5;
@ (g * f) = (@ g) * (@ f)
by A4, A5, A6, A7, A8, A9, ALTCAT_1:def 14;
then
UpperAdj (@ (g * f)) = (UpperAdj (@ f)) * (UpperAdj (@ g))
by A10, A11, Th9;
hence
( S2[a,b,f] & S2[b,c,g] implies S2[a,c,g * f] )
by WAYBEL20:29; verum