let C be non empty set ; :: thesis: for s, t being Element of holds
( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )
let s, t be Element of ; :: thesis: ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c )
( C,(@ s) @ = s & C,(@ t) @ = t ) ;
hence ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c ) by Th16; :: thesis: verum