let E, F, G be 1-sorted ; :: thesis: for x being object st x in [: the carrier of E, the carrier of F, the carrier of G:] holds
ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]
let x be object ; :: thesis: ( x in [: the carrier of E, the carrier of F, the carrier of G:] implies ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3] )
assume x in [: the carrier of E, the carrier of F, the carrier of G:] ; :: thesis: ex x1 being Point of E ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]
then consider x1, x2, x3 being object such that
A1: ( x1 in the carrier of E & x2 in the carrier of F & x3 in the carrier of G & x = [x1,x2,x3] ) by MCART_1:68;
reconsider x1 = x1 as Point of E by A1;
reconsider x2 = x2 as Point of F by A1;
reconsider x3 = x3 as Point of G by A1;
take x1 ; :: thesis: ex x2 being Point of F ex x3 being Point of G st x = [x1,x2,x3]
take x2 ; :: thesis: ex x3 being Point of G st x = [x1,x2,x3]
take x3 ; :: thesis: x = [x1,x2,x3]
thus x = [x1,x2,x3] by A1; :: thesis: verum