let U be Universe; :: thesis: for x being Element of U holds
( op0 x is Element of U & op1 x is Element of U & op2 x is Element of U )
let x be Element of U; :: thesis: ( op0 x is Element of U & op1 x is Element of U & op2 x is Element of U )
thus op0 x is Element of U ; :: thesis: ( op1 x is Element of U & op2 x is Element of U )
[:{x},{x}:] is Element of U ;
hence op1 x is Element of U ; :: thesis: op2 x is Element of U
[:[:{x},{x}:],{x}:] is Element of U ;
hence op2 x is Element of U by CLASSES4:13; :: thesis: verum