let OTS be OrdTrapSpace; :: thesis: for a', b', c' being Element of ex d' being Element of st a',b' // c',d'
let a', b', c' be Element of ; :: thesis: ex d' being Element of st a',b' // c',d'
reconsider a = a', b = b', c = c' as Element of by Th50;
consider d being Element of such that
A1: ( a,b // c,d or a,b // d,c ) by Def14;
reconsider d' = d as Element of by Th50;
take d' ; :: thesis: a',b' // c',d'
thus a',b' // c',d' by A1, Th51; :: thesis: verum