take a ; :: according to ORDINAL6:def 1 :: thesis: a \ b c= a
thus a \ b c= a ; :: thesis: verum