consider O12 being Function of (Outbds CPNT1),the carrier of CPNT2, O21 being Function of (Outbds CPNT2),the carrier of CPNT1;
set Z = [O12,O21];
take [O12,O21] ; :: thesis: ex O12 being Function of (Outbds CPNT1),the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2),the carrier of CPNT1 st [O12,O21] = [O12,O21]
thus ex O12 being Function of (Outbds CPNT1),the carrier of CPNT2 ex O21 being Function of (Outbds CPNT2),the carrier of CPNT1 st [O12,O21] = [O12,O21] ; :: thesis: verum