let FdSp be FanodesSp; :: thesis: for a, b, c, d being Element of FdSp st a,b congr c,d holds
c,d congr a,b
let a, b, c, d be Element of FdSp; :: thesis: ( a,b congr c,d implies c,d congr a,b )
assume a,b congr c,d ; :: thesis: c,d congr a,b
then ( a,b congr c,d & a,b congr a,b ) by Th66;
hence c,d congr a,b by Th67; :: thesis: verum