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