let o1, o2 be object of B; :: according to FUNCTOR0:def 19 :: thesis: ( <^o1,o2^> <> {} implies <^((incl B) . o1),((incl B) . o2)^> <> {} )
thus ( <^o1,o2^> <> {} implies <^((incl B) . o1),((incl B) . o2)^> <> {} ) by Th29, XBOOLE_1:3; :: thesis: verum