let L be 1-sorted ; :: thesis: for C being trivial Subset of L
for R being Relation of the carrier of L holds C is strict_chain of R
let C be trivial Subset of L; :: thesis: for R being Relation of the carrier of L holds C is strict_chain of R
let R be Relation of the carrier of L; :: thesis: C is strict_chain of R
let x, y be set ; :: according to WAYBEL35:def 3 :: thesis: ( x in C & y in C & not [x,y] in R & not x = y implies [y,x] in R )
thus ( x in C & y in C & not [x,y] in R & not x = y implies [y,x] in R ) by SUBSET_1:def 7; :: thesis: verum