set P = TolStr(# D,({} D,D) #);
thus
the ToleranceRel of TolStr(# D,({} D,D) #) is_irreflexive_in the carrier of TolStr(# D,({} D,D) #)
:: according to PCS_0:def 10 :: thesis: TolStr(# D,({} D,D) #) is pcs-tol-symmetric proof
let x be
set ;
:: according to RELAT_2:def 2 :: thesis: ( not x in the carrier of TolStr(# D,({} D,D) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} D,D) #) )
thus
( not
x in the
carrier of
TolStr(#
D,
({} D,D) #) or not
[^,^] in the
ToleranceRel of
TolStr(#
D,
({} D,D) #) )
;
:: thesis: verum
end;
let x be set ; :: according to RELAT_2:def 3,PCS_0:def 11 :: thesis: for b1 being set holds
( not x in the carrier of TolStr(# D,({} D,D) #) or not b1 in the carrier of TolStr(# D,({} D,D) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} D,D) #) or [^,^] in the ToleranceRel of TolStr(# D,({} D,D) #) )
thus
for b1 being set holds
( not x in the carrier of TolStr(# D,({} D,D) #) or not b1 in the carrier of TolStr(# D,({} D,D) #) or not [^,^] in the ToleranceRel of TolStr(# D,({} D,D) #) or [^,^] in the ToleranceRel of TolStr(# D,({} D,D) #) )
; :: thesis: verum